theory TEE_SEC_Common
imports "../GPTEE_Instantiation" "TEEC_SEC_Common"
begin
lemma tee_memories_setTaInsBusy : "∀s threadId isBusy. tee_memories (TEE_state s)
= tee_memories (TEE_state (setTaInsBusyByThreadId s threadId isBusy))"
proof-
{
fix s::"State"
fix threadId::"THREAD_ID_TYPE"
fix isBusy::"BUSY_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. threadId = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := isBusy⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have a1: "tee_memories (TEE_state s) = tee_memories (TEE_state (setTaInsBusyByThreadId s threadId isBusy))"
proof-
{
have b1: "setTaInsBusyByThreadId s threadId isBusy
= s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈"
by (metis setTaInsBusyByThreadId_def)
have b2: "tee_memories (TEE_state s) = tee_memories (TEE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈))"
by simp
have b3: "tee_memories (TEE_state s)
= tee_memories (TEE_state (setTaInsBusyByThreadId s threadId isBusy))"
using b1 b2 by presburger
then show ?thesis
by simp
}
qed
} then show ?thesis
by blast
qed
lemma tee_memories_setCurDomainAndEvent : "∀s currentID event. tee_memories (TEE_state s)
= tee_memories (TEE_state (setCurDomainAndEvent s currentID event))"
proof-
{
fix s::"State"
fix currentID::"DOMAIN_ID"
fix event::"(EVENT_PARAM × EVENT_NAME)"
have a1: "tee_memories (TEE_state s)
= tee_memories (TEE_state (setCurDomainAndEvent s currentID event))"
proof-
{
have b1: "setCurDomainAndEvent s currentID event
= s⦇current := currentID, exec_prime := event # (exec_prime s)⦈"
by (simp add: setCurDomainAndEvent_def)
have b2: "tee_memories (TEE_state (setCurDomainAndEvent s currentID event))
= tee_memories (TEE_state (s⦇current := currentID, exec_prime := event # (exec_prime s)⦈))"
by (simp add: b1)
have b3: "tee_memories (TEE_state s)
= tee_memories (TEE_state (setCurDomainAndEvent s currentID event))"
by (simp add: b1)
then show ?thesis
by simp
}
qed
} then show ?thesis
by simp
qed
lemma tee_memories_setTaInsBusy_setCurDomainAndEvent : "∀s threadId isBusy currentID event. tee_memories (TEE_state s) =
tee_memories (TEE_state (setCurDomainAndEvent (setTaInsBusyByThreadId s threadId isBusy) currentID event))"
using tee_memories_setCurDomainAndEvent tee_memories_setTaInsBusy by auto
lemma tee_invokeCmd_teeDomain : "∀sc s ses_id time_out cmd_id in_params out_params.
tee_memories (TEE_state s) = tee_memories (TEE_state (fst (tee_invokeTACommand_TEEDomain sc s ses_id time_out cmd_id in_params out_params)))"
proof-
{
fix sc s ses_id time_out cmd_id in_params out_params
let ?clientTid = "findSesCliTid s (the ses_id)"
let ?servTid = "findSesServTid s (the ses_id)"
let ?taInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?client_taIns = "getTAInsCtx s (the ?clientTid)"
let ?clnt_id = "ta_id ?client_taIns"
let ?taMgrSes = "the(getTASessionBySesIdFromMgr s (the ses_id))"
let ?curSesClintId = "the(id (client_id ?taMgrSes))"
let ?server_taIns = "getTAInsCtx s (the ?servTid)"
let ?isServTaBusy = "busy ?server_taIns"
let ?s_setServTaInsBusy = "setTaInsBusyByThreadId s (the ?servTid) True"
let ?exec = "(exec_prime s)"
let ?p = "fst (hd ?exec)"
let ?memblock = "the(param10 ?p)"
let ?memref = "the(param11 ?p)"
let ?memblock_memref = "TEE_pre_process (?memblock, ?memref) (the ?servTid)"
let ?param = "⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None, param5 = None,
param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
param10 = Some(fst ?memblock_memref), param11 = Some(snd ?memblock_memref), param12=None, param13=None⦈"
let ?s_addEvent = "setCurDomainAndEvent ?s_setServTaInsBusy (the ?servTid) (?param, TEE_IC3)"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. (the ?servTid) = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := True⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have "tee_memories (TEE_state s) = tee_memories (TEE_state (fst (tee_invokeTACommand_TEEDomain sc s ses_id time_out cmd_id in_params out_params)))"
proof(cases "ses_id = None ∨ cmd_id = None ∨ ?clientTid = None ∨ ?servTid = None ∨ ?clnt_id ≠ ?curSesClintId ∨ ?isServTaBusy = True")
case True
then have b1: "(fst (tee_invokeTACommand_TEEDomain sc s ses_id time_out cmd_id in_params out_params)) = s"
using tee_invokeTACommand_TEEDomain_def
by (smt (z3) fstI)
then show ?thesis
by simp
next
case False
then show ?thesis
proof-
{
have c1: "tee_memories (TEE_state s) = tee_memories (TEE_state (setTaInsBusyByThreadId s (the ?servTid) True))"
by (simp add: tee_memories_setTaInsBusy)
have c2: "(setTaInsBusyByThreadId s (the ?servTid) True) = ?s_setServTaInsBusy"
by simp
have c3: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s_setServTaInsBusy)"
by (simp add: c1)
have c4: "tee_memories (TEE_state ?s_setServTaInsBusy) = tee_memories (TEE_state ?s_addEvent)"
by (simp add: tee_memories_setCurDomainAndEvent)
have c5: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s_addEvent)"
by (simp add: c3 c4)
then show ?thesis
by (smt (z3) fstI tee_invokeTACommand_TEEDomain_def)
}
qed
qed
} then show ?thesis
by simp
qed
lemma ree_total_size_setTaInsBusy: "∀s threadId isBusy. ree_total_size (REE_state s)
= ree_total_size (REE_state (setTaInsBusyByThreadId s threadId isBusy))"
proof-
{
fix s::"State"
fix threadId::"THREAD_ID_TYPE"
fix isBusy::"BUSY_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. threadId = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := isBusy⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have a1: "ree_total_size (REE_state s) = ree_total_size (REE_state (setTaInsBusyByThreadId s threadId isBusy))"
proof-
{
have b1: "setTaInsBusyByThreadId s threadId isBusy
= s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈"
by (metis setTaInsBusyByThreadId_def)
have b2: "ree_total_size (REE_state s) = ree_total_size (REE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈))"
by simp
have b3: "ree_total_size (REE_state s)
= ree_total_size (REE_state (setTaInsBusyByThreadId s threadId isBusy))"
using b1 b2 by presburger
then show ?thesis
by simp
}
qed
} then show ?thesis
by blast
qed
lemma driver_mem_setTaInsBusy: "∀s threadId isBusy. driver_mem (REE_state s)
= driver_mem (REE_state (setTaInsBusyByThreadId s threadId isBusy))"
proof-
{
fix s::"State"
fix threadId::"THREAD_ID_TYPE"
fix isBusy::"BUSY_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. threadId = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := isBusy⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have a1: "driver_mem (REE_state s) = driver_mem (REE_state (setTaInsBusyByThreadId s threadId isBusy))"
proof-
{
have b1: "setTaInsBusyByThreadId s threadId isBusy
= s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈"
by (metis setTaInsBusyByThreadId_def)
have b2: "driver_mem (REE_state s) = driver_mem (REE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈))"
by simp
have b3: "driver_mem (REE_state s)
= driver_mem (REE_state (setTaInsBusyByThreadId s threadId isBusy))"
using b1 b2 by presburger
then show ?thesis
by simp
}
qed
} then show ?thesis
by blast
qed
lemma ree_total_size_setCurDomainAndEvent : "∀s currentID event. ree_total_size (REE_state s)
= ree_total_size (REE_state (setCurDomainAndEvent s currentID event))"
proof-
{
fix s::"State"
fix currentID::"DOMAIN_ID"
fix event::"(EVENT_PARAM × EVENT_NAME)"
have a1: "ree_total_size (REE_state s)
= ree_total_size (REE_state (setCurDomainAndEvent s currentID event))"
proof-
{
have b1: "setCurDomainAndEvent s currentID event
= s⦇current := currentID, exec_prime := event # (exec_prime s)⦈"
by (simp add: setCurDomainAndEvent_def)
have b2: "ree_total_size (REE_state (setCurDomainAndEvent s currentID event))
= ree_total_size (REE_state (s⦇current := currentID, exec_prime := event # (exec_prime s)⦈))"
by (simp add: b1)
have b3: "ree_total_size (REE_state s)
= ree_total_size (REE_state (setCurDomainAndEvent s currentID event))"
by (simp add: b1)
then show ?thesis
by simp
}
qed
} then show ?thesis
by simp
qed
lemma ree_total_size_tee_invokeTACommand_TEEDomain : "∀sc s ses_id time_out cmd_id in_params out_params.
ree_total_size (REE_state s) = ree_total_size (REE_state (fst (tee_invokeTACommand_TEEDomain sc s ses_id time_out cmd_id in_params out_params)))"
proof-
{
fix sc s ses_id time_out cmd_id in_params out_params
let ?clientTid = "findSesCliTid s (the ses_id)"
let ?servTid = "findSesServTid s (the ses_id)"
let ?taInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?client_taIns = "getTAInsCtx s (the ?clientTid)"
let ?clnt_id = "ta_id ?client_taIns"
let ?taMgrSes = "the(getTASessionBySesIdFromMgr s (the ses_id))"
let ?curSesClintId = "the(id (client_id ?taMgrSes))"
let ?server_taIns = "getTAInsCtx s (the ?servTid)"
let ?isServTaBusy = "busy ?server_taIns"
let ?s_setServTaInsBusy = "setTaInsBusyByThreadId s (the ?servTid) True"
let ?exec = "(exec_prime s)"
let ?p = "fst (hd ?exec)"
let ?memblock = "the(param10 ?p)"
let ?memref = "the(param11 ?p)"
let ?memblock_memref = "TEE_pre_process (?memblock, ?memref) (the ?servTid)"
let ?param = "⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None, param5 = None,
param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
param10 = Some(fst ?memblock_memref), param11 = Some(snd ?memblock_memref), param12=None, param13=None⦈"
let ?s_addEvent = "setCurDomainAndEvent ?s_setServTaInsBusy (the ?servTid) (?param, TEE_IC3)"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. (the ?servTid) = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := True⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have "ree_total_size (REE_state s) = ree_total_size (REE_state (fst (tee_invokeTACommand_TEEDomain sc s ses_id time_out cmd_id in_params out_params)))"
proof(cases "ses_id = None ∨ cmd_id = None ∨ ?clientTid = None ∨ ?servTid = None ∨ ?clnt_id ≠ ?curSesClintId ∨ ?isServTaBusy = True")
case True
then have b1: "(fst (tee_invokeTACommand_TEEDomain sc s ses_id time_out cmd_id in_params out_params)) = s"
using tee_invokeTACommand_TEEDomain_def
by (smt (z3) fstI)
then show ?thesis
by simp
next
case False
then show ?thesis
proof-
{
have c1: "ree_total_size (REE_state s) = ree_total_size (REE_state (setTaInsBusyByThreadId s (the ?servTid) True))"
by (simp add: ree_total_size_setTaInsBusy)
have c2: "(setTaInsBusyByThreadId s (the ?servTid) True) = ?s_setServTaInsBusy"
by simp
have c3: "ree_total_size (REE_state s) = ree_total_size (REE_state ?s_setServTaInsBusy)"
by (simp add: c1)
have c4: "ree_total_size (REE_state ?s_setServTaInsBusy) = ree_total_size (REE_state ?s_addEvent)"
by (simp add: ree_total_size_setCurDomainAndEvent)
have c5: "ree_total_size (REE_state s) = ree_total_size (REE_state ?s_addEvent)"
by (simp add: c3 c4)
then show ?thesis
by (smt (z3) fstI tee_invokeTACommand_TEEDomain_def)
}
qed
qed
} then show ?thesis
by simp
qed
lemma driver_mem_tee_setTaInsBusy: "∀s threadId isBusy. driver_mem(REE_state s)
= driver_mem(REE_state (setTaInsBusyByThreadId s threadId isBusy))"
proof-
{
fix s::"State"
fix threadId::"THREAD_ID_TYPE"
fix isBusy::"BUSY_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. threadId = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := isBusy⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have a1: "driver_mem(REE_state s) = driver_mem(REE_state (setTaInsBusyByThreadId s threadId isBusy))"
proof-
{
have b1: "setTaInsBusyByThreadId s threadId isBusy
= s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈"
by (metis setTaInsBusyByThreadId_def)
have b2: "driver_mem(REE_state s) = driver_mem(REE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈))"
by simp
have b3: "driver_mem(REE_state s)
= driver_mem(REE_state (setTaInsBusyByThreadId s threadId isBusy))"
using b1 b2 by presburger
then show ?thesis
by simp
}
qed
} then show ?thesis
by blast
qed
lemma driver_mem_tee_setCurDomainAndEvent : "∀s currentID event. driver_mem(REE_state s)
= driver_mem(REE_state (setCurDomainAndEvent s currentID event))"
proof-
{
fix s::"State"
fix currentID::"DOMAIN_ID"
fix event::"(EVENT_PARAM × EVENT_NAME)"
have a1: "driver_mem(REE_state s)
= driver_mem(REE_state (setCurDomainAndEvent s currentID event))"
proof-
{
have b1: "setCurDomainAndEvent s currentID event
= s⦇current := currentID, exec_prime := event # (exec_prime s)⦈"
by (simp add: setCurDomainAndEvent_def)
have b2: "driver_mem(REE_state (setCurDomainAndEvent s currentID event))
= driver_mem(REE_state (s⦇current := currentID, exec_prime := event # (exec_prime s)⦈))"
by (simp add: b1)
have b3: "driver_mem(REE_state s)
= driver_mem(REE_state (setCurDomainAndEvent s currentID event))"
by (simp add: b1)
then show ?thesis
by simp
}
qed
} then show ?thesis
by simp
qed
lemma driver_mem_tee_invokeTACommand_TEEDomain : "∀sc s ses_id time_out cmd_id in_params out_params.
driver_mem(REE_state s) = driver_mem(REE_state (fst (tee_invokeTACommand_TEEDomain sc s ses_id time_out cmd_id in_params out_params)))"
proof-
{
fix sc s ses_id time_out cmd_id in_params out_params
let ?clientTid = "findSesCliTid s (the ses_id)"
let ?servTid = "findSesServTid s (the ses_id)"
let ?taInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?client_taIns = "getTAInsCtx s (the ?clientTid)"
let ?clnt_id = "ta_id ?client_taIns"
let ?taMgrSes = "the(getTASessionBySesIdFromMgr s (the ses_id))"
let ?curSesClintId = "the(id (client_id ?taMgrSes))"
let ?server_taIns = "getTAInsCtx s (the ?servTid)"
let ?isServTaBusy = "busy ?server_taIns"
let ?s_setServTaInsBusy = "setTaInsBusyByThreadId s (the ?servTid) True"
let ?exec = "(exec_prime s)"
let ?p = "fst (hd ?exec)"
let ?memblock = "the(param10 ?p)"
let ?memref = "the(param11 ?p)"
let ?memblock_memref = "TEE_pre_process (?memblock, ?memref) (the ?servTid)"
let ?param = "⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None, param5 = None,
param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
param10 = Some(fst ?memblock_memref), param11 = Some(snd ?memblock_memref),
param12=None, param13=None⦈"
let ?s_addEvent = "setCurDomainAndEvent ?s_setServTaInsBusy (the ?servTid) (?param, TEE_IC3)"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. (the ?servTid) = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := True⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have " driver_mem(REE_state s) = driver_mem(REE_state (fst (tee_invokeTACommand_TEEDomain sc s ses_id time_out cmd_id in_params out_params)))"
proof(cases "ses_id = None ∨ cmd_id = None ∨ ?clientTid = None ∨ ?servTid = None ∨ ?clnt_id ≠ ?curSesClintId ∨ ?isServTaBusy = True")
case True
then have b1: "(fst (tee_invokeTACommand_TEEDomain sc s ses_id time_out cmd_id in_params out_params)) = s"
using tee_invokeTACommand_TEEDomain_def
by (smt (z3) fstI)
then show ?thesis
by simp
next
case False
then show ?thesis
proof-
{
have c1: "driver_mem(REE_state s) = driver_mem(REE_state (setTaInsBusyByThreadId s (the ?servTid) True))"
by (simp add: driver_mem_tee_setTaInsBusy)
have c2: "(setTaInsBusyByThreadId s (the ?servTid) True) = ?s_setServTaInsBusy"
by simp
have c3: "driver_mem(REE_state s) = driver_mem(REE_state ?s_setServTaInsBusy)"
by (simp add: c1)
have c4: "driver_mem(REE_state ?s_setServTaInsBusy) = driver_mem(REE_state ?s_addEvent)"
by (simp add: driver_mem_tee_setCurDomainAndEvent)
have c5: "driver_mem(REE_state s) = driver_mem(REE_state ?s_addEvent)"
by (simp add: c3 c4)
then show ?thesis
by (smt (z3) fstI tee_invokeTACommand_TEEDomain_def)
}
qed
qed
} then show ?thesis
by simp
qed
lemma tee_memories_TA_InvokeCommandEntryPoint :
assumes p1: "d ≠ tid"
shows "∀sc s cmd_id.
{x3. x3∈set(tee_memories(TEE_state s)) ∧ ownership x3 = d}
= {x4. x4∈set(tee_memories(TEE_state (TA_InvokeCommandEntryPoint sc s cmd_id tid))) ∧ ownership x4 = d}"
using TA_InvokeCommandEntryPoint_def
OpenSessionEntryPoint_not_change_mem TA_OpenSessionEntryPoint_def by auto
lemma tee_memories_exec_prime_tl :
"∀s. tee_memories (TEE_state s) = tee_memories (TEE_state (s⦇exec_prime := tl (exec_prime s)⦈))"
by simp
lemma ree_total_size_exec_prime_tl :
"ree_total_size(REE_state s) = ree_total_size (REE_state (s⦇exec_prime := tl (exec_prime s)⦈))"
by simp
lemma driver_mem_exec_prime_tl :
"driver_mem (REE_state s) = driver_mem (REE_state (s⦇exec_prime := tl (exec_prime s)⦈))"
by simp
lemma ree_total_size_TA_InvokeCommandEntryPoint:
"∀sc s cmd_id tid. ree_total_size(REE_state s) = ree_total_size(REE_state (TA_InvokeCommandEntryPoint sc s cmd_id tid))"
using TA_InvokeCommandEntryPoint_def
apply simp
apply(rule someI)
by (metis (mono_tags, lifting) verit_sko_ex')
lemma driver_mem_TA_InvokeCommandEntryPoint:
"∀sc s cmd_id tid. driver_mem(REE_state s) = driver_mem(REE_state (TA_InvokeCommandEntryPoint sc s cmd_id tid))"
using TA_InvokeCommandEntryPoint_def
apply simp
apply(rule someI)
by (metis (mono_tags, lifting) verit_sko_ex')
lemma tee_memories_tee_invokeTACommand_TEEDomain2: "∀sc s ses_id time_out cmd_id in_params out_params.
tee_memories (TEE_state s) = tee_memories (TEE_state (fst (tee_invokeTACommand_TEEDomain2 sc s ses_id time_out cmd_id in_params out_params)))"
proof-
{
fix sc s ses_id time_out cmd_id in_params out_params
let ?clientTid = "findSesCliTid s (the ses_id)"
let ?servTid = "findSesServTid s (the ses_id)"
let ?taInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?client_taIns = "getTAInsCtx s (the ?clientTid)"
let ?clnt_id = "ta_id ?client_taIns"
let ?taMgrSes = "the(getTASessionBySesIdFromMgr s (the ses_id))"
let ?curSesClintId = "the(id (client_id ?taMgrSes))"
let ?server_taIns = "getTAInsCtx s (the ?servTid)"
let ?isServTaBusy = "busy ?server_taIns"
let ?s_setServTaInsBusy = "setTaInsBusyByThreadId s (the ?servTid) True"
let ?exec = "(exec_prime s)"
let ?p = "fst (hd ?exec)"
let ?memblock = "the(param10 ?p)"
let ?memref = "the(param11 ?p)"
let ?memblock_memref = "TEE_pre_process (?memblock, ?memref) (the ?servTid)"
let ?param = "⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None,
param5 = None, param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
param10 = Some(fst ?memblock_memref), param11 = Some(snd ?memblock_memref),
param12=None, param13=None⦈"
let ?s_addEvent = "setCurDomainAndEvent ?s_setServTaInsBusy (the ?servTid) (?param, TEE_IC3)"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. (the ?servTid) = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := True⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have "tee_memories (TEE_state s) = tee_memories (TEE_state (fst (tee_invokeTACommand_TEEDomain2 sc s ses_id time_out cmd_id in_params out_params)))"
proof(cases "ses_id = None ∨ cmd_id = None ∨ ?clientTid = None ∨ ?servTid = None ∨ ?clnt_id ≠ ?curSesClintId ∨ ?isServTaBusy = True")
case True
then have b1: "(fst (tee_invokeTACommand_TEEDomain2 sc s ses_id time_out cmd_id in_params out_params)) = s"
using tee_invokeTACommand_TEEDomain2_def
by (smt (z3) fstI)
then show ?thesis
by simp
next
case False
then show ?thesis
proof-
{
have c1: "tee_memories (TEE_state s) = tee_memories (TEE_state (setTaInsBusyByThreadId s (the ?servTid) True))"
by (simp add: tee_memories_setTaInsBusy)
have c2: "(setTaInsBusyByThreadId s (the ?servTid) True) = ?s_setServTaInsBusy"
by simp
have c3: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s_setServTaInsBusy)"
by (simp add: c1)
have c4: "tee_memories (TEE_state ?s_setServTaInsBusy) = tee_memories (TEE_state ?s_addEvent)"
by (simp add: tee_memories_setCurDomainAndEvent)
have c5: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s_addEvent)"
by (simp add: c3 c4)
then show ?thesis
using c1 c2 c3 c4 c5 tee_invokeTACommand_TEEDomain2_def
by (smt (z3) fstI tee_memories_setCurDomainAndEvent)
}
qed
qed
} then show ?thesis by blast
qed
lemma ree_total_size_tee_invokeTACommand_TEEDomain2: "∀sc s ses_id time_out cmd_id in_params out_params.
ree_total_size (REE_state s) = ree_total_size (REE_state (fst (tee_invokeTACommand_TEEDomain2 sc s ses_id time_out cmd_id in_params out_params)))"
proof-
{
fix sc s ses_id time_out cmd_id in_params out_params
let ?clientTid = "findSesCliTid s (the ses_id)"
let ?servTid = "findSesServTid s (the ses_id)"
let ?taInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?client_taIns = "getTAInsCtx s (the ?clientTid)"
let ?clnt_id = "ta_id ?client_taIns"
let ?taMgrSes = "the(getTASessionBySesIdFromMgr s (the ses_id))"
let ?curSesClintId = "the(id (client_id ?taMgrSes))"
let ?server_taIns = "getTAInsCtx s (the ?servTid)"
let ?isServTaBusy = "busy ?server_taIns"
let ?s_setServTaInsBusy = "setTaInsBusyByThreadId s (the ?servTid) True"
let ?exec = "(exec_prime s)"
let ?p = "fst (hd ?exec)"
let ?memblock = "the(param10 ?p)"
let ?memref = "the(param11 ?p)"
let ?memblock_memref = "TEE_pre_process (?memblock, ?memref) (the ?servTid)"
let ?param = "⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None,
param5 = None, param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
param10 = Some(fst ?memblock_memref), param11 = Some(snd ?memblock_memref),
param12=None, param13=None⦈"
let ?s_addEvent = "setCurDomainAndEvent ?s_setServTaInsBusy (the ?servTid) (?param, TEE_IC3)"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. (the ?servTid) = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := True⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have "ree_total_size (REE_state s) = ree_total_size (REE_state (fst (tee_invokeTACommand_TEEDomain2 sc s ses_id time_out cmd_id in_params out_params)))"
proof(cases "ses_id = None ∨ cmd_id = None ∨ ?clientTid = None ∨ ?servTid = None ∨ ?clnt_id ≠ ?curSesClintId ∨ ?isServTaBusy = True")
case True
then have b1: "(fst (tee_invokeTACommand_TEEDomain2 sc s ses_id time_out cmd_id in_params out_params)) = s"
using tee_invokeTACommand_TEEDomain2_def
by (smt (z3) fstI)
then show ?thesis
by simp
next
case False
then show ?thesis
proof-
{
have c1: "ree_total_size (REE_state s) = ree_total_size (REE_state (setTaInsBusyByThreadId s (the ?servTid) True))"
by (simp add: ree_total_size_setTaInsBusy)
have c2: "(setTaInsBusyByThreadId s (the ?servTid) True) = ?s_setServTaInsBusy"
by simp
have c3: "ree_total_size (REE_state s) = ree_total_size (REE_state ?s_setServTaInsBusy)"
by (simp add: c1)
have c4: "ree_total_size (REE_state ?s_setServTaInsBusy) = ree_total_size (REE_state ?s_addEvent)"
by (simp add: ree_total_size_setCurDomainAndEvent)
have c5: "ree_total_size (REE_state s) = ree_total_size (REE_state ?s_addEvent)"
by (simp add: c3 c4)
then show ?thesis
using c1 c2 c3 c4 c5 tee_invokeTACommand_TEEDomain2_def
proof -
have "∀p. p = (fst p::State, snd p::TEE_RETURN_ORIGIN_TYPE × TEEC_RETURN_CODE_TYPE × PARAMS_TYPE option)"
by (meson prod.exhaust_sel)
then show ?thesis
by (smt (z3) Pair_inject c3 ree_total_size_setCurDomainAndEvent tee_invokeTACommand_TEEDomain2_def)
qed
}
qed
qed
} then show ?thesis
by simp
qed
lemma driver_mem_tee_invokeTACommand_TEEDomain2 : "∀sc s ses_id time_out cmd_id in_params out_params.
driver_mem(REE_state s) = driver_mem(REE_state (fst (tee_invokeTACommand_TEEDomain2 sc s ses_id time_out cmd_id in_params out_params)))"
proof-
{
fix sc s ses_id time_out cmd_id in_params out_params
let ?clientTid = "findSesCliTid s (the ses_id)"
let ?servTid = "findSesServTid s (the ses_id)"
let ?taInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?client_taIns = "getTAInsCtx s (the ?clientTid)"
let ?clnt_id = "ta_id ?client_taIns"
let ?taMgrSes = "the(getTASessionBySesIdFromMgr s (the ses_id))"
let ?curSesClintId = "the(id (client_id ?taMgrSes))"
let ?server_taIns = "getTAInsCtx s (the ?servTid)"
let ?isServTaBusy = "busy ?server_taIns"
let ?s_setServTaInsBusy = "setTaInsBusyByThreadId s (the ?servTid) True"
let ?exec = "(exec_prime s)"
let ?p = "fst (hd ?exec)"
let ?memblock = "the(param10 ?p)"
let ?memref = "the(param11 ?p)"
let ?memblock_memref = "TEE_pre_process (?memblock, ?memref) (the ?servTid)"
let ?param = "⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None,
param5 = None, param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
param10 = Some(fst ?memblock_memref), param11 = Some(snd ?memblock_memref),
param12=None, param13=None⦈"
let ?s_addEvent = "setCurDomainAndEvent ?s_setServTaInsBusy (the ?servTid) (?param, TEE_IC3)"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?index = "(SOME x. (the ?servTid) = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?isTaInsBusyNow = "busy ?taIns"
let ?taIns_update = "?taIns⦇busy := True⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
have " driver_mem(REE_state s) = driver_mem(REE_state (fst (tee_invokeTACommand_TEEDomain2 sc s ses_id time_out cmd_id in_params out_params)))"
proof(cases "ses_id = None ∨ cmd_id = None ∨ ?clientTid = None ∨ ?servTid = None ∨ ?clnt_id ≠ ?curSesClintId ∨ ?isServTaBusy = True")
case True
then have b1: "(fst (tee_invokeTACommand_TEEDomain2 sc s ses_id time_out cmd_id in_params out_params)) = s"
using tee_invokeTACommand_TEEDomain2_def
by (smt (z3) fstI)
then show ?thesis
by simp
next
case False
then show ?thesis
proof-
{
have c1: "driver_mem(REE_state s) = driver_mem(REE_state (setTaInsBusyByThreadId s (the ?servTid) True))"
by (simp add: driver_mem_tee_setTaInsBusy)
have c2: "(setTaInsBusyByThreadId s (the ?servTid) True) = ?s_setServTaInsBusy"
by simp
have c3: "driver_mem(REE_state s) = driver_mem(REE_state ?s_setServTaInsBusy)"
by (simp add: c1)
have c4: "driver_mem(REE_state ?s_setServTaInsBusy) = driver_mem(REE_state ?s_addEvent)"
by (simp add: driver_mem_tee_setCurDomainAndEvent)
have c5: "driver_mem(REE_state s) = driver_mem(REE_state ?s_addEvent)"
by (simp add: c3 c4)
then show ?thesis
using c1 c2 c3 c4 c5
proof -
have "∀p. p = (fst p::State, snd p::TEE_RETURN_ORIGIN_TYPE × TEEC_RETURN_CODE_TYPE × PARAMS_TYPE option)"
by (meson prod.exhaust_sel)
then show ?thesis
by (smt (z3) Pair_inject c3 driver_mem_tee_setCurDomainAndEvent tee_invokeTACommand_TEEDomain2_def)
qed
}
qed
qed
} then show ?thesis
by simp
qed
lemma ree_total_size_removeSessionInContext: "∀s fd ses_id.
ree_total_size(REE_state (removeSessionInContext s fd ses_id)) = ree_total_size(REE_state s)"
proof-
{
fix s::"State"
fix fd::"FD_TYPE"
fix ses_id::"SESSION_ID_TYPE"
let ?tmp = "(tee_ctx_list (REE_state s))"
let ?index = "(SOME x. fd = ctx_fd (?tmp!x))"
have a0: "ree_total_size(REE_state (removeSessionInContext s fd ses_id))
= ree_total_size(REE_state (s⦇REE_state := (REE_state s)⦇
tee_ctx_list := list_update ?tmp ?index
⦇ctx_fd=fd,reg_mem=False,
driver_session_list=remove1 ses_id (driver_session_list (?tmp!?index))
⦈⦈⦈))"
using removeSessionInContext_def
by metis
have a1: "ree_total_size(REE_state (s⦇REE_state := (REE_state s)⦇
tee_ctx_list := list_update ?tmp ?index
⦇ctx_fd=fd,reg_mem=False,
driver_session_list=remove1 ses_id (driver_session_list (?tmp!?index))
⦈⦈⦈)) = ree_total_size(REE_state s)"
apply simp
done
have a2: "ree_total_size(REE_state (removeSessionInContext s fd ses_id)) = ree_total_size(REE_state s)"
using a0 a1 by metis
} then show ?thesis by blast
qed
lemma driver_mem_removeSessionInContext: "∀s fd ses_id.
driver_mem(REE_state (removeSessionInContext s fd ses_id)) = driver_mem(REE_state s)"
proof-
{
fix s::"State"
fix fd::"FD_TYPE"
fix ses_id::"SESSION_ID_TYPE"
let ?tmp = "(tee_ctx_list (REE_state s))"
let ?index = "(SOME x. fd = ctx_fd (?tmp!x))"
have a0: "driver_mem(REE_state (removeSessionInContext s fd ses_id))
= driver_mem(REE_state (s⦇REE_state := (REE_state s)⦇
tee_ctx_list := list_update ?tmp ?index
⦇ctx_fd=fd,reg_mem=False,
driver_session_list=remove1 ses_id (driver_session_list (?tmp!?index))
⦈⦈⦈))"
using removeSessionInContext_def
by metis
have a1: "driver_mem(REE_state (s⦇REE_state := (REE_state s)⦇
tee_ctx_list := list_update ?tmp ?index
⦇ctx_fd=fd,reg_mem=False,
driver_session_list=remove1 ses_id (driver_session_list (?tmp!?index))
⦈⦈⦈)) = driver_mem(REE_state s)"
apply simp
done
have a2: "driver_mem(REE_state (removeSessionInContext s fd ses_id)) = driver_mem(REE_state s)"
using a0 a1 by metis
} then show ?thesis by blast
qed
lemma tee_memories_removeSessionInContext: "∀s fd ses_id. tee_memories (TEE_state s)
= tee_memories (TEE_state (removeSessionInContext s fd ses_id))"
proof-
{
fix s::"State"
fix fd::"FD_TYPE"
fix ses_id::"SESSION_ID_TYPE"
let ?tmp = "(tee_ctx_list (REE_state s))"
let ?index = "(SOME x. fd = ctx_fd (?tmp!x))"
have a1: "tee_memories (TEE_state s)
= tee_memories (TEE_state (removeSessionInContext s fd ses_id))"
proof-
{
have b1: "removeSessionInContext s fd ses_id
= s⦇REE_state := (REE_state s)⦇
tee_ctx_list := list_update ?tmp ?index
⦇ctx_fd=fd,reg_mem=False,
driver_session_list=remove1 ses_id (driver_session_list (?tmp!?index))⦈⦈⦈"
by (metis removeSessionInContext_def)
have b2: "tee_memories (TEE_state (removeSessionInContext s fd ses_id))
=tee_memories (TEE_state (s⦇REE_state := (REE_state s)⦇
tee_ctx_list := list_update ?tmp ?index
⦇ctx_fd=fd,reg_mem=False,
driver_session_list=remove1 ses_id (driver_session_list (?tmp!?index))⦈⦈⦈))"
by (simp add: b1)
have b3: "tee_memories (TEE_state s)
= tee_memories (TEE_state (s⦇REE_state := (REE_state s)⦇
tee_ctx_list := list_update ?tmp ?index
⦇ctx_fd=fd,reg_mem=False,
driver_session_list=remove1 ses_id (driver_session_list (?tmp!?index))⦈⦈⦈))"
apply simp
done
have b4: "tee_memories (TEE_state s)
= tee_memories (TEE_state (removeSessionInContext s fd ses_id))"
using b1 b2 b3
by presburger
then show ?thesis by simp
}
qed
} then show ?thesis by auto
qed
lemma mgr_ta_sessions_findSesServTid: "∀s t ses_id ses_id_t.
ses_id = ses_id_t ∧ mgr_ta_sessions (ta_mgr (TEE_state s)) = mgr_ta_sessions (ta_mgr (TEE_state t))
⟶ findSesServTid s ses_id = findSesServTid t ses_id_t"
proof-
{
fix s::"State"
fix t::"State"
fix ses_id::"SESSION_ID_TYPE"
fix ses_id_t::"SESSION_ID_TYPE"
let ?mgrTaSesList = "mgr_ta_sessions (ta_mgr (TEE_state s))"
let ?mgrTaSes = "findTaSesInMgrBySesId ?mgrTaSesList ses_id"
let ?mgrTaSesList_t = "mgr_ta_sessions (ta_mgr (TEE_state t))"
let ?mgrTaSes_t = "findTaSesInMgrBySesId ?mgrTaSesList_t ses_id_t"
assume a1: "ses_id = ses_id_t"
assume a2: "mgr_ta_sessions (ta_mgr (TEE_state s)) = mgr_ta_sessions (ta_mgr (TEE_state t))"
have b1: "?mgrTaSesList = ?mgrTaSesList_t"
by (simp add: a2)
have b2: "ses_id = ses_id_t"
by (simp add: a1)
have b3: "?mgrTaSes = ?mgrTaSes_t"
by (simp add: b1 b2)
have b4: "findSesServTid s ses_id = findSesServTid t ses_id_t"
by (simp add: b3 findSesServTid_def)
} then show ?thesis
by blast
qed
lemma mgr_ta_sessions_findSesCliTid: "∀s t ses_id ses_id_t.
ses_id = ses_id_t ∧ ta_mgr (TEE_state s) = ta_mgr (TEE_state t)
⟶ findSesCliTid s ses_id = findSesCliTid t ses_id_t"
proof-
{
fix s::"State"
fix t::"State"
fix ses_id::"SESSION_ID_TYPE"
fix ses_id_t::"SESSION_ID_TYPE"
let ?taInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?taIns_opt = "findTaInsInMgrBySesId ?taInsList ses_id"
let ?taInsList_t = "mgr_ta_instances (ta_mgr (TEE_state t))"
let ?taIns_opt_t = "findTaInsInMgrBySesId ?taInsList ses_id_t"
assume a1: "ses_id = ses_id_t"
assume a2: "ta_mgr (TEE_state s) = ta_mgr (TEE_state t)"
have b1: "?taInsList = ?taInsList_t"
using a2 by simp
have b2: "findTaInsInMgrBySesId ?taInsList ses_id = findTaInsInMgrBySesId ?taInsList_t ses_id_t"
using a1 b1
by simp
have b3: "findSesCliTid s ses_id = findSesCliTid t ses_id_t"
by (simp add: a1 a2 findSesCliTid_def)
} then show ?thesis
by metis
qed
lemma getTAInsCtx_mgr_ta_instances: "∀ s t tid tid_t.
tid = tid_t ∧ ta_mgr (TEE_state s) = ta_mgr (TEE_state t)
⟶ getTAInsCtx s tid = getTAInsCtx t tid_t"
proof-
{
fix s::"State"
fix t::"State"
fix tid::"THREAD_ID_TYPE"
fix tid_t::"THREAD_ID_TYPE"
assume a1: "tid = tid_t"
assume a2: "ta_mgr (TEE_state s) = ta_mgr (TEE_state t)"
let ?mgrTaInsCtxs = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?mgrTaInsCtxs_t = "mgr_ta_instances (ta_mgr (TEE_state t))"
have b1: "mgr_ta_instances (ta_mgr (TEE_state s)) = mgr_ta_instances (ta_mgr (TEE_state t))"
by (simp add: a2)
have b2: "(SOME x. tid = cur_ta_thread_id (?mgrTaInsCtxs!x)) = (SOME x. tid = cur_ta_thread_id (?mgrTaInsCtxs_t!x))"
by (simp add: a2)
} then show ?thesis
using getTAInsCtx_def by presburger
qed
lemma isSessIdInTaInsSessList_cur_ta_session_list: "∀ s ses_id t ses_id_t.
ses_id = ses_id_t ∧ ta_mgr (TEE_state s) = ta_mgr (TEE_state t)
⟶ isSessIdInTaInsSessList (cur_ta_session_list (getTAInsCtx s (the (findSesCliTid s (the ses_id))))) (the ses_id)
= isSessIdInTaInsSessList (cur_ta_session_list (getTAInsCtx t (the (findSesCliTid t (the ses_id_t))))) (the ses_id_t)"
proof-
{
fix s::"State"
fix t::"State"
fix ses_id::"SESSION_ID_TYPE option"
fix ses_id_t::"SESSION_ID_TYPE option"
let ?clientTaIns = "(getTAInsCtx s (the (findSesCliTid s (the ses_id))))"
let ?clientTaIns_t = "(getTAInsCtx t (the (findSesCliTid t (the ses_id_t))))"
let ?isSessIdinSessIdList = "isSessIdInTaInsSessList (cur_ta_session_list ?clientTaIns) (the ses_id)"
let ?isSessIdinSessIdList_t = "isSessIdInTaInsSessList (cur_ta_session_list ?clientTaIns_t) (the ses_id_t)"
assume a1: "ses_id = ses_id_t"
assume a2: "ta_mgr (TEE_state s) = ta_mgr (TEE_state t)"
have b1: "findSesCliTid s (the ses_id) = findSesCliTid t (the ses_id_t)"
using a1 a2 mgr_ta_sessions_findSesCliTid by blast
have b2: "?clientTaIns = ?clientTaIns_t"
using getTAInsCtx_mgr_ta_instances
by (metis a2 b1)
have b3: "?isSessIdinSessIdList = ?isSessIdinSessIdList_t"
by (metis a1 b2)
} then show ?thesis
by blast
qed
lemma driver_mem_subtractMgrInsRef: "∀s tid.
driver_mem(REE_state s) = driver_mem(REE_state (fst (subtractMgrInsRef s tid)))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?isTaTidInList = "isTidInTaInsList ?mgrTaInsList tid"
let ?index = "(SOME x. tid = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?taIns_update = "⦇ta_id = ta_id ?taIns, cur_ta_session_list = cur_ta_session_list ?taIns,
reference_cnt = (reference_cnt ?taIns) - 1, busy = (busy ?taIns),
cur_ta_thread_id = cur_ta_thread_id ?taIns, attribute = attribute ?taIns⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
let ?s_plusTaInsRef = "s⦇TEE_state := (TEE_state s)⦇ta_mgr := (ta_mgr(TEE_state s))⦇mgr_ta_instances := ?mgrTaInsList_update⦈⦈⦈"
have "driver_mem(REE_state s) = driver_mem(REE_state (fst (subtractMgrInsRef s tid)))"
proof-
{
have a1: "(fst (subtractMgrInsRef s tid))
= s⦇TEE_state := (TEE_state s)⦇ta_mgr := (ta_mgr(TEE_state s))⦇mgr_ta_instances := ?mgrTaInsList_update⦈⦈⦈"
using subtractMgrInsRef_def
by (metis fst_conv)
then show ?thesis by auto
}
qed
} then show ?thesis by blast
qed
lemma driver_mem_removeAllSessIdInTaStateSessList: "∀s ses_id params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (removeAllSessIdInTaStateSessList s ses_id params_in params_out))"
proof-
{
fix s::"State"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?servTid = "the(findSesServTid s ses_id)"
let ?ta_state_map = "TAs_state s"
let ?ta_state = "the(?ta_state_map ?servTid)"
let ?ta_state_sessions = "TA_sessions ?ta_state"
let ?lst_drop_index = "removeAll ses_id ?ta_state_sessions"
let ?ta_state_update = "?ta_state⦇TA_sessions := ?lst_drop_index⦈"
let ?ta_state_map_update = "?ta_state_map(?servTid := Some ?ta_state_update)"
let ?s_ret = "s⦇TAs_state := ?ta_state_map_update⦈"
have a1: "driver_mem(REE_state s) = driver_mem(REE_state (removeAllSessIdInTaStateSessList s ses_id params_in params_out))"
proof-
{
have b1: "removeAllSessIdInTaStateSessList s ses_id params_in params_out
= s⦇TAs_state := ?ta_state_map_update⦈"
by (metis removeAllSessIdInTaStateSessList_def)
have b2: "driver_mem(REE_state s) = driver_mem(REE_state (s⦇TAs_state := ?ta_state_map_update⦈))"
by simp
then show ?thesis
using b1 by auto
}
qed
} then show ?thesis by blast
qed
lemma driver_mem_removeTaInsInMgrInsList: "∀s tid.
driver_mem(REE_state s) = driver_mem(REE_state (fst (removeTaInsInMgrInsList s tid)))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?isTaTidInList = "isTidInTaInsList ?mgrTaInsList tid"
let ?mgrTaInsList_removeAllTaInns = "removeAllTaInsInMgrInsList tid ?mgrTaInsList"
let ?s_ret = "s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_removeAllTaInns⦈⦈⦈"
have "driver_mem(REE_state s) = driver_mem(REE_state (fst (removeTaInsInMgrInsList s tid)))"
proof(cases "?isTaTidInList = False")
case True
have a1: "?isTaTidInList = False"
by (simp add: True)
then show ?thesis
proof-
{
have b1: "fst (removeTaInsInMgrInsList s tid) = s"
using removeTaInsInMgrInsList_def a1
by simp
then show ?thesis
by simp
}
qed
next
case False
have a2: "?isTaTidInList = True"
using False by auto
then show ?thesis
proof-
{
have c1: "fst (removeTaInsInMgrInsList s tid)
= s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_removeAllTaInns⦈⦈⦈"
using removeTaInsInMgrInsList_def a2
by simp
then show ?thesis by auto
}
qed
qed
} then show ?thesis by blast
qed
lemma driver_mem_removeTaMemInTeeDomain: "∀s tid.
driver_mem(REE_state s) = driver_mem(REE_state (removeTaMemInTeeDomain s tid))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
let ?teeMemList = "tee_memories (TEE_state s)"
let ?curTidMemSize = "calMemBlockInMemBlockList tid ?teeMemList"
let ?newTeeMemList = "removeAllMemBlockInMemBlockList tid ?teeMemList"
let ?newTotal = "(tee_total_size (TEE_state s)) + ?curTidMemSize"
have "driver_mem(REE_state s) = driver_mem(REE_state (removeTaMemInTeeDomain s tid))"
proof-
{
have a1: "removeTaMemInTeeDomain s tid =
s⦇TEE_state := (TEE_state s)⦇tee_total_size := ?newTotal, tee_memories := ?newTeeMemList⦈⦈"
by (metis removeTaMemInTeeDomain_def)
then show ?thesis by auto
}
qed
} then show ?thesis by blast
qed
lemma driver_mem_close_session_teeDomain: "∀sc s ses_id params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (fst (close_session_teeDomain sc s ses_id params_in params_out)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?servTid = "the(findSesServTid s ses_id)"
let ?servTaIns = "getTAInsCtx s ?servTid"
let ?client_tid = "the(findSesCliTid s ses_id)"
let ?mgrTaInsCtxs = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?clientTaIns = "getTAInsCtx s ?client_tid"
let ?isSessIdinSessIdList = "isSessIdInTaInsSessList (cur_ta_session_list ?clientTaIns) ses_id"
let ?mgrSes = "the(findMgrSessionFromList s ses_id)"
let ?clientType = "client_id ?mgrSes"
let ?loginType = "login ?clientType"
let ?s_removeSess_inMgrTaIns = "removeAllSessIdInTaInsSessList s ?client_tid ses_id params_in params_out"
let ?s_removeSess_inMgrTaSes = "removeAllSessionInMgrSesList ?s_removeSess_inMgrTaIns ses_id"
let ?s_removeSess_inTaState = "removeAllSessIdInTaStateSessList ?s_removeSess_inMgrTaSes ses_id params_in params_out"
let ?s_setBusy = "setTaInsBusyByThreadId ?s_removeSess_inTaState ?servTid False"
let ?s_subRef = "subtractMgrInsRef ?s_setBusy ?servTid"
let ?s_subRef_state = "fst ?s_subRef"
let ?mgrTaInsCtxs_update = "mgr_ta_instances (ta_mgr (TEE_state ?s_subRef_state))"
let ?index = "(SOME x. ?servTid = cur_ta_thread_id (?mgrTaInsCtxs_update!x))"
let ?servTaIns_update = "?mgrTaInsCtxs_update!?index"
let ?servTa_refCnt = "reference_cnt ?servTaIns_update"
let ?cur_ta_attr = "TA_INSTANCE_CTX_TYPE.attribute ?servTaIns_update"
let ?isSingleInstance = "singleInstance ?cur_ta_attr"
let ?isKeepAlive = "keepAlive ?cur_ta_attr"
let ?s_removeTaInTaIns = "removeTaInsInMgrInsList (fst ?s_subRef) ?servTid"
let ?s_removeTaMemInTee = "removeTaMemInTeeDomain (fst ?s_removeTaInTaIns) ?servTid"
let ?param = "⦇param1 = Some ses_id, param2 = None, param3 = None, param4 = None,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out,
param9 = Some ?servTaIns, param10=None, param11=None, param12=None, param13=None⦈"
let ?s_destoryTaContext = "?s_removeTaMemInTee⦇current := ?servTid, exec_prime:=(?param, TEE_CS3)#(exec_prime ?s_removeTaMemInTee)⦈"
have "driver_mem(REE_state s) = driver_mem(REE_state (fst (close_session_teeDomain sc s ses_id params_in params_out)))"
proof(cases "?isSessIdinSessIdList = False")
case True
have a1: "?isSessIdinSessIdList = False"
by (simp add: True)
then show ?thesis
proof-
{
have b1: "(fst (close_session_teeDomain sc s ses_id params_in params_out)) = s"
using a1 close_session_teeDomain_def by simp
then show ?thesis
by simp
}
qed
next
case False
have a2: "?isSessIdinSessIdList = True"
using False by auto
then show ?thesis
proof(cases "?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)")
case True
have a3: "?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)"
using True by auto
then show ?thesis
proof-
{
have c0: "¬(?isSessIdinSessIdList = False) ∧ (?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY))"
using False a3 by blast
have c1: "(fst (close_session_teeDomain sc s ses_id params_in params_out)) = ?s_destoryTaContext"
using c0 close_session_teeDomain_def fst_conv
apply simp
by (metis fst_conv)
have c2: "driver_mem(REE_state s) = driver_mem(REE_state ?s_removeSess_inMgrTaIns)"
by (metis (no_types, lifting) State.ext_inject State.surjective State.update_convs(4) removeAllSessIdInTaInsSessList_def)
have c3: "driver_mem(REE_state ?s_removeSess_inMgrTaIns) = driver_mem(REE_state ?s_removeSess_inMgrTaSes)"
by (simp add: removeAllSessionInMgrSesList_def)
have c4_0: "driver_mem(REE_state ?s_removeSess_inMgrTaSes) = driver_mem(REE_state ?s_removeSess_inTaState)"
by (metis State.ext_inject State.surjective State.update_convs(2) removeAllSessIdInTaStateSessList_def)
have c4: "driver_mem(REE_state ?s_removeSess_inTaState) = driver_mem(REE_state ?s_setBusy)"
by (simp add: driver_mem_tee_setTaInsBusy)
have c5: "driver_mem(REE_state ?s_setBusy) = driver_mem(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))"
using driver_mem_subtractMgrInsRef
by simp
have c6: "driver_mem(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))
= driver_mem(REE_state (fst ?s_removeTaInTaIns))"
using driver_mem_removeTaInsInMgrInsList
by simp
have c7: "driver_mem(REE_state (fst ?s_removeTaInTaIns)) = driver_mem(REE_state ?s_removeTaMemInTee)"
using driver_mem_removeTaMemInTeeDomain
by simp
have c8: "driver_mem(REE_state ?s_removeTaMemInTee)
= driver_mem(REE_state (?s_removeTaMemInTee⦇current := ?servTid, exec_prime:=(?param, TEE_CS3)#(exec_prime ?s_removeTaMemInTee)⦈))"
by simp
then show ?thesis
using c1 c2 c3 c4 c4_0 c5 c6 c7 by presburger
}
qed
next
case False
have a4: "¬(?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY))"
using False by auto
then show ?thesis
proof-
{
have d0: "¬(?isSessIdinSessIdList = False) ∧ (¬(?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)))"
using False a2 by blast
have d1: "(fst (close_session_teeDomain sc s ses_id params_in params_out)) = ?s_subRef_state"
using d0 close_session_teeDomain_def fst_conv
by (smt (z3) Eps_cong)
have d2: "driver_mem(REE_state s) = driver_mem(REE_state ?s_removeSess_inMgrTaIns)"
by (metis (no_types, lifting) State.ext_inject State.surjective State.update_convs(4) removeAllSessIdInTaInsSessList_def)
have d3: "driver_mem(REE_state ?s_removeSess_inMgrTaIns) = driver_mem(REE_state ?s_removeSess_inMgrTaSes)"
by (simp add: removeAllSessionInMgrSesList_def)
have d4_0: "driver_mem(REE_state ?s_removeSess_inMgrTaSes) = driver_mem(REE_state ?s_removeSess_inTaState)"
by (simp add: driver_mem_removeAllSessIdInTaStateSessList)
have d4: "driver_mem(REE_state ?s_removeSess_inMgrTaSes) = driver_mem(REE_state ?s_setBusy)"
by (simp add: d4_0 driver_mem_tee_setTaInsBusy)
have d5: "driver_mem(REE_state ?s_setBusy) = driver_mem(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))"
using driver_mem_subtractMgrInsRef
by simp
then show ?thesis
by (simp add: d1 d2 d3 d4)
}
qed
qed
qed
} then show ?thesis by blast
qed
lemma driver_mem_close_session_teeDomain2: "∀sc s ses_id params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (fst (close_session_teeDomain2 sc s ses_id params_in params_out)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?servTid = "the(findSesServTid s ses_id)"
let ?servTaIns = "getTAInsCtx s ?servTid"
let ?client_tid = "the(findSesCliTid s ses_id)"
let ?mgrTaInsCtxs = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?clientTaIns = "getTAInsCtx s ?client_tid"
let ?isSessIdinSessIdList = "isSessIdInTaInsSessList (cur_ta_session_list ?clientTaIns) ses_id"
let ?mgrSes = "the(findMgrSessionFromList s ses_id)"
let ?clientType = "client_id ?mgrSes"
let ?loginType = "login ?clientType"
let ?s_removeSess_inMgrTaIns = "removeAllSessIdInTaInsSessList s ?client_tid ses_id params_in params_out"
let ?s_removeSess_inMgrTaSes = "removeAllSessionInMgrSesList ?s_removeSess_inMgrTaIns ses_id"
let ?s_removeSess_inTaState = "removeAllSessIdInTaStateSessList ?s_removeSess_inMgrTaSes ses_id params_in params_out"
let ?s_setBusy = "setTaInsBusyByThreadId ?s_removeSess_inTaState ?servTid False"
let ?s_subRef = "subtractMgrInsRef ?s_setBusy ?servTid"
let ?s_subRef_state = "fst ?s_subRef"
let ?mgrTaInsCtxs_update = "mgr_ta_instances (ta_mgr (TEE_state ?s_subRef_state))"
let ?index = "(SOME x. ?servTid = cur_ta_thread_id (?mgrTaInsCtxs_update!x))"
let ?servTaIns_update = "?mgrTaInsCtxs_update!?index"
let ?servTa_refCnt = "reference_cnt ?servTaIns_update"
let ?cur_ta_attr = "TA_INSTANCE_CTX_TYPE.attribute ?servTaIns_update"
let ?isSingleInstance = "singleInstance ?cur_ta_attr"
let ?isKeepAlive = "keepAlive ?cur_ta_attr"
let ?s_removeTaInTaIns = "removeTaInsInMgrInsList (fst ?s_subRef) ?servTid"
let ?s_removeTaMemInTee = "removeTaMemInTeeDomain (fst ?s_removeTaInTaIns) ?servTid"
let ?param = "⦇param1 = Some ses_id, param2 = None, param3 = None, param4 = None,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = Some ?servTaIns,
param10=None, param11=None, param12=None, param13=None⦈"
let ?s_destoryTaContext = "?s_removeTaMemInTee⦇current := ?servTid, exec_prime:=(?param, TEEC_CS3)#(exec_prime ?s_removeTaMemInTee)⦈"
have "driver_mem(REE_state s) = driver_mem(REE_state (fst (close_session_teeDomain2 sc s ses_id params_in params_out)))"
proof(cases "?isSessIdinSessIdList = False")
case True
have a1: "?isSessIdinSessIdList = False"
by (simp add: True)
then show ?thesis
proof-
{
have b1: "(fst (close_session_teeDomain2 sc s ses_id params_in params_out)) = s"
using a1 close_session_teeDomain2_def by simp
then show ?thesis
by simp
}
qed
next
case False
have a2: "?isSessIdinSessIdList = True"
using False by auto
then show ?thesis
proof(cases "?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)")
case True
have a3: "?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)"
using True by auto
then show ?thesis
proof-
{
have c0: "¬(?isSessIdinSessIdList = False) ∧ (?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY))"
using False a3 by blast
have c1: "(fst (close_session_teeDomain2 sc s ses_id params_in params_out)) = ?s_destoryTaContext"
using c0 close_session_teeDomain2_def fst_conv
apply simp
by (metis fst_conv)
have c2: "driver_mem(REE_state s) = driver_mem(REE_state ?s_removeSess_inMgrTaIns)"
by (metis (no_types, lifting) State.ext_inject State.surjective State.update_convs(4) removeAllSessIdInTaInsSessList_def)
have c3: "driver_mem(REE_state ?s_removeSess_inMgrTaIns) = driver_mem(REE_state ?s_removeSess_inMgrTaSes)"
by (simp add: removeAllSessionInMgrSesList_def)
have c4_0: "driver_mem(REE_state ?s_removeSess_inMgrTaSes) = driver_mem(REE_state ?s_removeSess_inTaState)"
by (simp add: driver_mem_removeAllSessIdInTaStateSessList)
have c4: "driver_mem(REE_state ?s_removeSess_inTaState) = driver_mem(REE_state ?s_setBusy)"
by (simp add: driver_mem_tee_setTaInsBusy)
have c5: "driver_mem(REE_state ?s_setBusy) = driver_mem(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))"
using driver_mem_subtractMgrInsRef
by simp
have c6: "driver_mem(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))
= driver_mem(REE_state (fst ?s_removeTaInTaIns))"
using driver_mem_removeTaInsInMgrInsList
by simp
have c7: "driver_mem(REE_state (fst ?s_removeTaInTaIns)) = driver_mem(REE_state ?s_removeTaMemInTee)"
using driver_mem_removeTaMemInTeeDomain
by simp
have c8: "driver_mem(REE_state ?s_removeTaMemInTee)
= driver_mem(REE_state (?s_removeTaMemInTee⦇current := ?servTid, exec_prime:=(?param, TEEC_CS3)#(exec_prime ?s_removeTaMemInTee)⦈))"
by simp
then show ?thesis
using c1 c2 c3 c4_0 c4 c5 c6 c7 by presburger
}
qed
next
case False
have a4: "¬(?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY))"
using False by auto
then show ?thesis
proof-
{
have d0: "¬(?isSessIdinSessIdList = False) ∧ (¬(?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)))"
using False a2 by blast
have d1: "(fst (close_session_teeDomain2 sc s ses_id params_in params_out)) = ?s_subRef_state"
using d0 close_session_teeDomain2_def fst_conv
apply simp
by (smt (z3) a4 fst_eqD)
have d2: "driver_mem(REE_state s) = driver_mem(REE_state ?s_removeSess_inMgrTaIns)"
by (metis (no_types, lifting) State.ext_inject State.surjective State.update_convs(4) removeAllSessIdInTaInsSessList_def)
have d3: "driver_mem(REE_state ?s_removeSess_inMgrTaIns) = driver_mem(REE_state ?s_removeSess_inMgrTaSes)"
by (simp add: removeAllSessionInMgrSesList_def)
have d4_0: "driver_mem(REE_state ?s_removeSess_inMgrTaSes) = driver_mem(REE_state ?s_removeSess_inTaState)"
by (simp add: driver_mem_removeAllSessIdInTaStateSessList)
have d4: "driver_mem(REE_state ?s_removeSess_inTaState) = driver_mem(REE_state ?s_setBusy)"
by (simp add: driver_mem_tee_setTaInsBusy)
have d5: "driver_mem(REE_state ?s_setBusy) = driver_mem(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))"
using driver_mem_subtractMgrInsRef
by simp
then show ?thesis
by (simp add: d1 d2 d3 d4 d4_0 d5)
}
qed
qed
qed
} then show ?thesis by blast
qed
lemma ree_total_size_subtractMgrInsRef: "∀s tid.
ree_total_size(REE_state s) = ree_total_size(REE_state (fst (subtractMgrInsRef s tid)))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?isTaTidInList = "isTidInTaInsList ?mgrTaInsList tid"
let ?index = "(SOME x. tid = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?taIns_update = "⦇ta_id = ta_id ?taIns, cur_ta_session_list = cur_ta_session_list ?taIns,
reference_cnt = (reference_cnt ?taIns) - 1, busy = (busy ?taIns),
cur_ta_thread_id = cur_ta_thread_id ?taIns, attribute = attribute ?taIns⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
let ?s_plusTaInsRef = "s⦇TEE_state := (TEE_state s)⦇ta_mgr := (ta_mgr(TEE_state s))⦇mgr_ta_instances := ?mgrTaInsList_update⦈⦈⦈"
have "ree_total_size(REE_state s) = ree_total_size(REE_state (fst (subtractMgrInsRef s tid)))"
proof-
{
have a1: "(fst (subtractMgrInsRef s tid))
= s⦇TEE_state := (TEE_state s)⦇ta_mgr := (ta_mgr(TEE_state s))⦇mgr_ta_instances := ?mgrTaInsList_update⦈⦈⦈"
using subtractMgrInsRef_def
by (metis fst_conv)
then show ?thesis by auto
}
qed
} then show ?thesis by blast
qed
lemma ree_total_size_removeTaInsInMgrInsList: "∀s tid.
ree_total_size(REE_state s) = ree_total_size(REE_state (fst (removeTaInsInMgrInsList s tid)))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?isTaTidInList = "isTidInTaInsList ?mgrTaInsList tid"
let ?mgrTaInsList_removeAllTaInns = "removeAllTaInsInMgrInsList tid ?mgrTaInsList"
let ?s_ret = "s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_removeAllTaInns⦈⦈⦈"
have "ree_total_size(REE_state s) = ree_total_size(REE_state (fst (removeTaInsInMgrInsList s tid)))"
proof(cases "?isTaTidInList = False")
case True
have a1: "?isTaTidInList = False"
by (simp add: True)
then show ?thesis
proof-
{
have b1: "fst (removeTaInsInMgrInsList s tid) = s"
using removeTaInsInMgrInsList_def a1
by simp
then show ?thesis
by simp
}
qed
next
case False
have a2: "?isTaTidInList = True"
using False by auto
then show ?thesis
proof-
{
have c1: "fst (removeTaInsInMgrInsList s tid)
= s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_removeAllTaInns⦈⦈⦈"
using removeAllTaInsInMgrInsList_def a2
by (simp add: removeTaInsInMgrInsList_def)
then show ?thesis by auto
}
qed
qed
} then show ?thesis by blast
qed
lemma ree_total_size_removeTaMemInTeeDomain: "∀s tid.
ree_total_size(REE_state s) = ree_total_size(REE_state (removeTaMemInTeeDomain s tid))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
let ?teeMemList = "tee_memories (TEE_state s)"
let ?curTidMemSize = "calMemBlockInMemBlockList tid ?teeMemList"
let ?newTeeMemList = "removeAllMemBlockInMemBlockList tid ?teeMemList"
let ?newTotal = "(tee_total_size (TEE_state s)) + ?curTidMemSize"
have "ree_total_size(REE_state s) = ree_total_size(REE_state (removeTaMemInTeeDomain s tid))"
proof-
{
have a1: "removeTaMemInTeeDomain s tid =
s⦇TEE_state := (TEE_state s)⦇tee_total_size := ?newTotal, tee_memories := ?newTeeMemList⦈⦈"
by (metis removeTaMemInTeeDomain_def)
then show ?thesis by auto
}
qed
} then show ?thesis by blast
qed
lemma ree_total_size_removeAllSessIdInTaStateSessList: "∀s ses_id params_in params_out.
ree_total_size(REE_state s) = ree_total_size(REE_state (removeAllSessIdInTaStateSessList s ses_id params_in params_out))"
proof-
{
fix s::"State"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?servTid = "the(findSesServTid s ses_id)"
let ?ta_state_map = "TAs_state s"
let ?ta_state = "the(?ta_state_map ?servTid)"
let ?ta_state_sessions = "TA_sessions ?ta_state"
let ?lst_drop_index = "removeAll ses_id ?ta_state_sessions"
let ?ta_state_update = "?ta_state⦇TA_sessions := ?lst_drop_index⦈"
let ?ta_state_map_update = "?ta_state_map(?servTid := Some ?ta_state_update)"
let ?s_ret = "s⦇TAs_state := ?ta_state_map_update⦈"
have a1: "ree_total_size(REE_state s) = ree_total_size(REE_state (removeAllSessIdInTaStateSessList s ses_id params_in params_out))"
proof-
{
have b1: "removeAllSessIdInTaStateSessList s ses_id params_in params_out
= s⦇TAs_state := ?ta_state_map_update⦈"
by (metis removeAllSessIdInTaStateSessList_def)
have b2: "ree_total_size(REE_state s) = ree_total_size(REE_state (s⦇TAs_state := ?ta_state_map_update⦈))"
by simp
then show ?thesis
using b1 by auto
}
qed
} then show ?thesis by blast
qed
lemma ree_total_size_close_session_teeDomain: "∀sc s ses_id params_in params_out.
ree_total_size(REE_state s) = ree_total_size(REE_state (fst (close_session_teeDomain sc s ses_id params_in params_out)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?servTid = "the(findSesServTid s ses_id)"
let ?servTaIns = "getTAInsCtx s ?servTid"
let ?client_tid = "the(findSesCliTid s ses_id)"
let ?mgrTaInsCtxs = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?clientTaIns = "getTAInsCtx s ?client_tid"
let ?isSessIdinSessIdList = "isSessIdInTaInsSessList (cur_ta_session_list ?clientTaIns) ses_id"
let ?mgrSes = "the(findMgrSessionFromList s ses_id)"
let ?clientType = "client_id ?mgrSes"
let ?loginType = "login ?clientType"
let ?s_removeSess_inMgrTaIns = "removeAllSessIdInTaInsSessList s ?client_tid ses_id params_in params_out"
let ?s_removeSess_inMgrTaSes = "removeAllSessionInMgrSesList ?s_removeSess_inMgrTaIns ses_id"
let ?s_removeSess_inTaState = "removeAllSessIdInTaStateSessList ?s_removeSess_inMgrTaSes ses_id params_in params_out"
let ?s_setBusy = "setTaInsBusyByThreadId ?s_removeSess_inTaState ?servTid False"
let ?s_subRef = "subtractMgrInsRef ?s_setBusy ?servTid"
let ?s_subRef_state = "fst ?s_subRef"
let ?mgrTaInsCtxs_update = "mgr_ta_instances (ta_mgr (TEE_state ?s_subRef_state))"
let ?index = "(SOME x. ?servTid = cur_ta_thread_id (?mgrTaInsCtxs_update!x))"
let ?servTaIns_update = "?mgrTaInsCtxs_update!?index"
let ?servTa_refCnt = "reference_cnt ?servTaIns_update"
let ?cur_ta_attr = "attribute ?servTaIns_update"
let ?isSingleInstance = "singleInstance ?cur_ta_attr"
let ?isKeepAlive = "keepAlive ?cur_ta_attr"
let ?s_removeTaInTaIns = "removeTaInsInMgrInsList (fst ?s_subRef) ?servTid"
let ?s_removeTaMemInTee = "removeTaMemInTeeDomain (fst ?s_removeTaInTaIns) ?servTid"
let ?param = "⦇param1 = Some ses_id, param2 = None, param3 = None, param4 = None,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = Some ?servTaIns,
param10 = None, param11 = None, param12=None, param13=None⦈"
let ?s_destoryTaContext = "?s_removeTaMemInTee⦇current := ?servTid, exec_prime:=(?param, TEE_CS3)#(exec_prime ?s_removeTaMemInTee)⦈"
have "ree_total_size(REE_state s) = ree_total_size(REE_state (fst (close_session_teeDomain sc s ses_id params_in params_out)))"
proof(cases "?isSessIdinSessIdList = False")
case True
have a1: "?isSessIdinSessIdList = False"
by (simp add: True)
then show ?thesis
proof-
{
have b1: "(fst (close_session_teeDomain sc s ses_id params_in params_out)) = s"
using a1 close_session_teeDomain_def by simp
then show ?thesis
by simp
}
qed
next
case False
have a2: "?isSessIdinSessIdList = True"
using False by auto
then show ?thesis
proof(cases "?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)")
case True
have a3: "?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)"
using True by auto
then show ?thesis
proof-
{
have c0: "¬(?isSessIdinSessIdList = False) ∧ (?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY))"
using False a3 by blast
have c1: "(fst (close_session_teeDomain sc s ses_id params_in params_out)) = ?s_destoryTaContext"
using c0 close_session_teeDomain_def fst_conv
apply simp
by (metis fst_conv)
have c2: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s_removeSess_inMgrTaIns)"
by (metis (no_types, lifting) State.ext_inject State.surjective State.update_convs(4) removeAllSessIdInTaInsSessList_def)
have c3: "ree_total_size(REE_state ?s_removeSess_inMgrTaIns) = ree_total_size(REE_state ?s_removeSess_inMgrTaSes)"
by (simp add: removeAllSessionInMgrSesList_def)
have c4_0: "ree_total_size(REE_state ?s_removeSess_inMgrTaSes) = ree_total_size(REE_state ?s_removeSess_inTaState)"
by (simp add: ree_total_size_removeAllSessIdInTaStateSessList)
have c4: "ree_total_size(REE_state ?s_removeSess_inMgrTaSes) = ree_total_size(REE_state ?s_removeSess_inTaState)"
by (simp add: c4_0)
have c5: "ree_total_size(REE_state ?s_setBusy) = ree_total_size(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))"
by (simp add: ree_total_size_subtractMgrInsRef)
have c6: "ree_total_size(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))
= ree_total_size(REE_state (fst ?s_removeTaInTaIns))"
by (simp add: ree_total_size_removeTaInsInMgrInsList)
have c7: "ree_total_size(REE_state (fst ?s_removeTaInTaIns)) = ree_total_size(REE_state ?s_removeTaMemInTee)"
by (simp add: ree_total_size_removeTaMemInTeeDomain)
have c8: "ree_total_size(REE_state ?s_removeTaMemInTee)
= ree_total_size(REE_state (?s_removeTaMemInTee⦇current := ?servTid, exec_prime:=(?param, TEE_CS3)#(exec_prime ?s_removeTaMemInTee)⦈))"
by simp
then show ?thesis
using c1 c2 c3 c4_0 c4 c5 c6 c7
by (metis ree_total_size_setTaInsBusy)
}
qed
next
case False
have a4: "¬(?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY))"
using False by auto
then show ?thesis
proof-
{
have d0: "¬(?isSessIdinSessIdList = False) ∧ (¬(?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)))"
using False a2 by blast
have d1: "(fst (close_session_teeDomain sc s ses_id params_in params_out)) = ?s_subRef_state"
using d0 close_session_teeDomain_def fst_conv
apply simp
by (smt (z3) a4 fst_eqD)
have d2: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s_removeSess_inMgrTaIns)"
by (metis (no_types, lifting) State.ext_inject State.surjective State.update_convs(4) removeAllSessIdInTaInsSessList_def)
have d3: "ree_total_size(REE_state ?s_removeSess_inMgrTaIns) = ree_total_size(REE_state ?s_removeSess_inMgrTaSes)"
by (simp add: removeAllSessionInMgrSesList_def)
have d4_0: "ree_total_size(REE_state ?s_removeSess_inMgrTaSes) = ree_total_size(REE_state ?s_removeSess_inTaState)"
by (simp add: ree_total_size_removeAllSessIdInTaStateSessList)
have d4: "ree_total_size(REE_state ?s_removeSess_inTaState) = ree_total_size(REE_state ?s_setBusy)"
by (simp add: ree_total_size_setTaInsBusy)
have d5: "ree_total_size(REE_state ?s_setBusy) = ree_total_size(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))"
by (simp add: ree_total_size_subtractMgrInsRef)
then show ?thesis
by (simp add: d1 d2 d3 d4 d4_0)
}
qed
qed
qed
} then show ?thesis by blast
qed
lemma ree_total_size_close_session_teeDomain2: "∀sc s ses_id params_in params_out.
ree_total_size(REE_state s) = ree_total_size(REE_state (fst (close_session_teeDomain2 sc s ses_id params_in params_out)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?servTid = "the(findSesServTid s ses_id)"
let ?servTaIns = "getTAInsCtx s ?servTid"
let ?client_tid = "the(findSesCliTid s ses_id)"
let ?mgrTaInsCtxs = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?clientTaIns = "getTAInsCtx s ?client_tid"
let ?isSessIdinSessIdList = "isSessIdInTaInsSessList (cur_ta_session_list ?clientTaIns) ses_id"
let ?mgrSes = "the(findMgrSessionFromList s ses_id)"
let ?clientType = "client_id ?mgrSes"
let ?loginType = "login ?clientType"
let ?s_removeSess_inMgrTaIns = "removeAllSessIdInTaInsSessList s ?client_tid ses_id params_in params_out"
let ?s_removeSess_inMgrTaSes = "removeAllSessionInMgrSesList ?s_removeSess_inMgrTaIns ses_id"
let ?s_removeSess_inTaState = "removeAllSessIdInTaStateSessList ?s_removeSess_inMgrTaSes ses_id params_in params_out"
let ?s_setBusy = "setTaInsBusyByThreadId ?s_removeSess_inTaState ?servTid False"
let ?s_subRef = "subtractMgrInsRef ?s_setBusy ?servTid"
let ?s_subRef_state = "fst ?s_subRef"
let ?mgrTaInsCtxs_update = "mgr_ta_instances (ta_mgr (TEE_state ?s_subRef_state))"
let ?index = "(SOME x. ?servTid = cur_ta_thread_id (?mgrTaInsCtxs_update!x))"
let ?servTaIns_update = "?mgrTaInsCtxs_update!?index"
let ?servTa_refCnt = "reference_cnt ?servTaIns_update"
let ?cur_ta_attr = "TA_INSTANCE_CTX_TYPE.attribute ?servTaIns_update"
let ?isSingleInstance = "singleInstance ?cur_ta_attr"
let ?isKeepAlive = "keepAlive ?cur_ta_attr"
let ?s_removeTaInTaIns = "removeTaInsInMgrInsList (fst ?s_subRef) ?servTid"
let ?s_removeTaMemInTee = "removeTaMemInTeeDomain (fst ?s_removeTaInTaIns) ?servTid"
let ?param = "⦇param1 = Some ses_id, param2 = None, param3 = None, param4 = None,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = Some ?servTaIns,
param10 = None, param11=None, param12=None, param13=None⦈"
let ?s_destoryTaContext = "?s_removeTaMemInTee⦇current := ?servTid, exec_prime:=(?param, TEEC_CS3)#(exec_prime ?s_removeTaMemInTee)⦈"
have "ree_total_size(REE_state s) = ree_total_size(REE_state (fst (close_session_teeDomain2 sc s ses_id params_in params_out)))"
proof(cases "?isSessIdinSessIdList = False")
case True
have a1: "?isSessIdinSessIdList = False"
by (simp add: True)
then show ?thesis
proof-
{
have b1: "(fst (close_session_teeDomain2 sc s ses_id params_in params_out)) = s"
using a1 close_session_teeDomain2_def by simp
then show ?thesis
by simp
}
qed
next
case False
have a2: "?isSessIdinSessIdList = True"
using False by auto
then show ?thesis
proof(cases "?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)")
case True
have a3: "?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)"
using True by auto
then show ?thesis
proof-
{
have c0: "¬(?isSessIdinSessIdList = False) ∧ (?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY))"
using False a3 by blast
have c1: "(fst (close_session_teeDomain2 sc s ses_id params_in params_out)) = ?s_destoryTaContext"
using c0 close_session_teeDomain2_def fst_conv
apply simp
by (meson fst_conv)
have c2: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s_removeSess_inMgrTaIns)"
by (metis (no_types, lifting) State.ext_inject State.surjective State.update_convs(4) removeAllSessIdInTaInsSessList_def)
have c3: "ree_total_size(REE_state ?s_removeSess_inMgrTaIns) = ree_total_size(REE_state ?s_removeSess_inMgrTaSes)"
by (simp add: removeAllSessionInMgrSesList_def)
have c4_0: "ree_total_size(REE_state ?s_removeSess_inMgrTaSes) = ree_total_size(REE_state ?s_removeSess_inTaState)"
by (metis State.ext_inject State.surjective State.update_convs(2) removeAllSessIdInTaStateSessList_def)
have c4: "ree_total_size(REE_state ?s_removeSess_inTaState) = ree_total_size(REE_state ?s_setBusy)"
by (simp add: ree_total_size_setTaInsBusy)
have c5: "ree_total_size(REE_state ?s_setBusy) = ree_total_size(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))"
by (simp add: ree_total_size_subtractMgrInsRef)
have c6: "ree_total_size(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))
= ree_total_size(REE_state (fst ?s_removeTaInTaIns))"
by (simp add: ree_total_size_removeTaInsInMgrInsList)
have c7: "ree_total_size(REE_state (fst ?s_removeTaInTaIns)) = ree_total_size(REE_state ?s_removeTaMemInTee)"
by (simp add: ree_total_size_removeTaMemInTeeDomain)
have c8: "ree_total_size(REE_state ?s_removeTaMemInTee)
= ree_total_size(REE_state (?s_removeTaMemInTee⦇current := ?servTid, exec_prime:=(?param, TEEC_CS3)#(exec_prime ?s_removeTaMemInTee)⦈))"
by simp
then show ?thesis
using c1 c2 c3 c4_0 c4 c5 c6 c7 by presburger
}
qed
next
case False
have a4: "¬(?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY))"
using False by auto
then show ?thesis
proof-
{
have d0: "¬(?isSessIdinSessIdList = False) ∧ (¬(?servTa_refCnt = 0 ∧ (?isKeepAlive = False | ?loginType = DTC_IDENTITY)))"
using False a2 by blast
have d1: "(fst (close_session_teeDomain2 sc s ses_id params_in params_out)) = ?s_subRef_state"
using d0 close_session_teeDomain2_def fst_conv
apply simp
by (smt (z3) fst_conv less_numeral_extra(3))
have d2: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s_removeSess_inMgrTaIns)"
by (metis (no_types, lifting) State.ext_inject State.surjective State.update_convs(4) removeAllSessIdInTaInsSessList_def)
have d3: "ree_total_size(REE_state ?s_removeSess_inMgrTaIns) = ree_total_size(REE_state ?s_removeSess_inMgrTaSes)"
by (simp add: removeAllSessionInMgrSesList_def)
have d4_0: "ree_total_size(REE_state ?s_removeSess_inMgrTaSes) = ree_total_size(REE_state ?s_removeSess_inTaState)"
by (metis State.ext_inject State.surjective State.update_convs(2) removeAllSessIdInTaStateSessList_def)
have d4: "ree_total_size(REE_state ?s_removeSess_inTaState) = ree_total_size(REE_state ?s_setBusy)"
by (simp add: ree_total_size_setTaInsBusy)
have d5: "ree_total_size(REE_state ?s_setBusy) = ree_total_size(REE_state (fst (subtractMgrInsRef ?s_setBusy ?servTid)))"
by (simp add: ree_total_size_subtractMgrInsRef)
then show ?thesis
by (simp add: d1 d2 d3 d4_0 d4 d5)
}
qed
qed
qed
} then show ?thesis by simp
qed
lemma current_tee_memories: "∀s sc.
tee_memories (TEE_state s) = tee_memories (TEE_state (s⦇current := TEE sc⦈))"
by simp
lemma current_ree_total_size: "∀s sc.
ree_total_size(REE_state s) = ree_total_size(REE_state (s⦇current := TEE sc⦈))"
by simp
lemma current_driver_mem: "∀s sc.
driver_mem(REE_state s) = driver_mem(REE_state (s⦇current := TEE sc⦈))"
by simp
lemma isSesIdinMgrSesList_cur_ta_session_list: "∀ s ses_id t ses_id_t.
ses_id = ses_id_t ∧ ta_mgr (TEE_state s) = ta_mgr (TEE_state t)
⟶ isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the ses_id)
= isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state t))) (the ses_id_t)"
proof-
{
fix s::"State"
fix t::"State"
fix ses_id::"SESSION_ID_TYPE option"
fix ses_id_t::"SESSION_ID_TYPE option"
let ?isSesIdinMgrSesList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the ses_id)"
let ?isSesIdinMgrSesList_t = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state t))) (the ses_id_t)"
assume a1: "ses_id = ses_id_t"
assume a2: "ta_mgr (TEE_state s) = ta_mgr (TEE_state t)"
have b1: "(mgr_ta_sessions (ta_mgr (TEE_state s))) = (mgr_ta_sessions (ta_mgr (TEE_state t)))"
using a1 a2 by auto
have b2: "?isSesIdinMgrSesList = ?isSesIdinMgrSesList_t"
using b1 a1 by auto
} then show ?thesis
by auto
qed
lemma TA_InvokeCommandEntryPoint_about_TEE:"∀s sc cmd_id tid. ( filter (λx. block_id x=(0::nat)) (tee_memories(TEE_state (TA_InvokeCommandEntryPoint sc s cmd_id tid)) )
=( filter (λx. block_id x=(0::nat)) (tee_memories(TEE_state s))))"
using TA_InvokeCommandEntryPoint_def apply simp
apply(rule someI)
using some_eq_imp
by (metis (mono_tags, lifting) )
lemma TA_InvokeCommandEntryPoint_about_other_TA:"∀s sc cmd_id tid. ( filter (λx. ownership x≠tid) (tee_memories(TEE_state (TA_InvokeCommandEntryPoint sc s cmd_id tid)) )
=( filter (λx. ownership x≠tid) (tee_memories(TEE_state s))))"
using TA_InvokeCommandEntryPoint_def apply simp
apply(rule someI)
using some_eq_imp
by (metis (mono_tags, lifting))
lemma TA_InvokeCommandEntryPoint_not_change_TEE_aux:"({x. x∈set(tee_memories (TEE_state (s)))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state (TA_InvokeCommandEntryPoint sc s cmd_id tid)))∧ (block_id x=0)})"
using TA_InvokeCommandEntryPoint_about_TEE filter_related by fastforce
lemma TA_InvokeCommandEntryPoint_not_change_TEE:"∀s sc tid cmd_id. ({x. x∈set(tee_memories (TEE_state (s)))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state (TA_InvokeCommandEntryPoint sc s cmd_id tid)))∧ (block_id x=0)})"
using TA_InvokeCommandEntryPoint_not_change_TEE_aux by blast
lemma TA_InvokeCommandEntryPoint_not_change_other_TA_aux:"{x. x∈set((tee_memories (TEE_state s)))∧ (ownership x≠tid)} =
{x. x∈set((tee_memories (TEE_state (TA_InvokeCommandEntryPoint sc s cmd_id tid))))∧ (ownership x≠tid)}"
proof -
have "⋀n s. filter (λm. ownership m ≠ n) (tee_memories (TEE_state (SOME sa. REE_state (sa::State) = REE_state (s::State) ∧ filter (λm. block_id m = 0) (tee_memories (TEE_state sa)) = filter (λm. block_id m = 0) (tee_memories (TEE_state s)) ∧ filter (λm. ownership m ≠ n) (tee_memories (TEE_state sa)) = filter (λm. ownership m ≠ n) (tee_memories (TEE_state s))))) = filter (λm. ownership m ≠ n) (tee_memories (TEE_state s))"
using TA_InvokeCommandEntryPoint_about_other_TA TA_InvokeCommandEntryPoint_def
by (smt (verit, ccfv_SIG) some_eq_imp)
then have "{m ∈ set (tee_memories (TEE_state (SOME sa. REE_state (sa::State) = REE_state s ∧ filter (λm. block_id m = 0) (tee_memories (TEE_state sa)) = filter (λm. block_id m = 0) (tee_memories (TEE_state s)) ∧ filter (λm. ownership m ≠ tid) (tee_memories (TEE_state sa)) = filter (λm. ownership m ≠ tid) (tee_memories (TEE_state s))))). ownership m ≠ tid} = {m ∈ set (tee_memories (TEE_state s)). ownership m ≠ tid}"
using filter_related_TA by blast
then show ?thesis
using TA_InvokeCommandEntryPoint_def
using OpenSessionEntryPoint_not_change_other_TA_aux TA_OpenSessionEntryPoint_def by auto
qed
lemma TA_InvokeCommandEntryPoint_not_change_other_TA:"∀sc s cmd_id tid. {x. x∈set((tee_memories (TEE_state s)))∧ (ownership x≠tid)} =
{x. x∈set((tee_memories (TEE_state (TA_InvokeCommandEntryPoint sc s cmd_id tid))))∧ (ownership x≠tid)}"
using TA_InvokeCommandEntryPoint_not_change_other_TA_aux by blast
lemma CloseSessionEntryPoint_about_TEE:"∀s sc tid. ( filter (λx. block_id x=(0::nat)) (tee_memories(TEE_state (TA_CloseSessionEntryPoint s tid)) )
=( filter (λx. block_id x=(0::nat)) (tee_memories(TEE_state s))))"
using TA_CloseSessionEntryPoint_def apply simp
apply(rule someI)
using some_eq_imp
by (metis (mono_tags, lifting) )
lemma CloseSessionEntryPoint_about_other_TA:"∀s sc opt tid. ( filter (λx. ownership x≠tid) (tee_memories(TEE_state (TA_CloseSessionEntryPoint s tid)) )
=( filter (λx. ownership x≠tid) (tee_memories(TEE_state s))))"
using TA_CloseSessionEntryPoint_def apply simp
apply(rule someI)
using some_eq_imp
by (metis (mono_tags, lifting) )
lemma CloseSessionEntryPoint_not_change_TEE_aux:"({x. x∈set(tee_memories (TEE_state (s)))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state (TA_CloseSessionEntryPoint s tid)))∧ (block_id x=0)})"
using CloseSessionEntryPoint_about_TEE filter_related by fastforce
lemma CloseSessionEntryPoint_not_change_TEE:"∀s tid. ({x. x∈set(tee_memories (TEE_state (s)))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state (TA_CloseSessionEntryPoint s tid)))∧ (block_id x=0)})"
using CloseSessionEntryPoint_not_change_TEE_aux by blast
lemma CloseSessionEntryPoint_not_change_other_TA_aux:"{x. x∈set((tee_memories (TEE_state s)))∧ (ownership x≠tid)} =
{x. x∈set((tee_memories (TEE_state (TA_CloseSessionEntryPoint s tid))))∧ (ownership x≠tid)}"
proof -
have "⋀n s. filter (λm. ownership m ≠ n) (tee_memories (TEE_state (SOME sa. REE_state (sa::State) = REE_state (s::State) ∧ filter (λm. block_id m = 0) (tee_memories (TEE_state sa)) = filter (λm. block_id m = 0) (tee_memories (TEE_state s)) ∧ filter (λm. ownership m ≠ n) (tee_memories (TEE_state sa)) = filter (λm. ownership m ≠ n) (tee_memories (TEE_state s))))) = filter (λm. ownership m ≠ n) (tee_memories (TEE_state s))"
using OpenSessionEntryPoint_about_other_TA TA_OpenSessionEntryPoint_def
by (smt (verit, del_insts) some_eq_imp)
then have "{m ∈ set (tee_memories (TEE_state (SOME sa. REE_state (sa::State) = REE_state s ∧ filter (λm. block_id m = 0) (tee_memories (TEE_state sa)) = filter (λm. block_id m = 0) (tee_memories (TEE_state s)) ∧ filter (λm. ownership m ≠ tid) (tee_memories (TEE_state sa)) = filter (λm. ownership m ≠ tid) (tee_memories (TEE_state s))))). ownership m ≠ tid} = {m ∈ set (tee_memories (TEE_state s)). ownership m ≠ tid}"
using filter_related_TA by blast
then show ?thesis
using TA_CloseSessionEntryPoint_def
using TA_InvokeCommandEntryPoint_def TA_InvokeCommandEntryPoint_not_change_other_TA_aux by presburger
qed
lemma CloseSessionEntryPoint_not_change_other_TA:"∀s sc opt tid. {x. x∈set((tee_memories (TEE_state s)))∧ (ownership x≠tid)} =
{x. x∈set((tee_memories (TEE_state (TA_CloseSessionEntryPoint s tid))))∧ (ownership x≠tid)}"
using CloseSessionEntryPoint_not_change_other_TA_aux by blast
lemma tee_memories_removeAllSessIdInTaStateSessList: "∀s ses_id params_in params_out. tee_memories (TEE_state s)
= tee_memories (TEE_state (removeAllSessIdInTaStateSessList s ses_id params_in params_out))"
proof-
{
fix s::"State"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?servTid = "the(findSesServTid s ses_id)"
let ?ta_state_map = "TAs_state s"
let ?ta_state = "the(?ta_state_map ?servTid)"
let ?ta_state_sessions = "TA_sessions ?ta_state"
let ?lst_drop_index = "removeAll ses_id ?ta_state_sessions"
let ?ta_state_update = "?ta_state⦇TA_sessions := ?lst_drop_index⦈"
let ?ta_state_map_update = "?ta_state_map(?servTid := Some ?ta_state_update)"
let ?s_ret = "s⦇TAs_state := ?ta_state_map_update⦈"
have a1: "tee_memories (TEE_state s)
= tee_memories (TEE_state (removeAllSessIdInTaStateSessList s ses_id params_in params_out))"
proof-
{
have b1: "removeAllSessIdInTaStateSessList s ses_id params_in params_out = s⦇TAs_state := ?ta_state_map_update⦈"
by (metis removeAllSessIdInTaStateSessList_def)
have b2: "tee_memories (TEE_state s) = tee_memories (TEE_state (s⦇TAs_state := ?ta_state_map_update⦈))"
by simp
have b3: "tee_memories (TEE_state s)
= tee_memories (TEE_state (removeAllSessIdInTaStateSessList s ses_id params_in params_out))"
using b1 b2 by presburger
then show ?thesis
by simp
}
qed
} then show ?thesis by simp
qed
lemma tee_memories_subtractMgrInsRef: "∀s tid.
tee_memories (TEE_state s) = tee_memories (TEE_state (fst (subtractMgrInsRef s tid)))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?isTaTidInList = "isTidInTaInsList ?mgrTaInsList tid"
let ?index = "(SOME x. tid = cur_ta_thread_id (?mgrTaInsList!x))"
let ?taIns = "?mgrTaInsList!?index"
let ?taIns_update = "⦇ta_id = ta_id ?taIns, cur_ta_session_list = cur_ta_session_list ?taIns,
reference_cnt = (reference_cnt ?taIns) - 1, busy = (busy ?taIns),
cur_ta_thread_id = cur_ta_thread_id ?taIns, attribute = attribute ?taIns⦈"
let ?mgrTaInsList_update = "list_update ?mgrTaInsList ?index ?taIns_update"
let ?s_plusTaInsRef = "s⦇TEE_state := (TEE_state s)⦇ta_mgr := (ta_mgr(TEE_state s))⦇mgr_ta_instances := ?mgrTaInsList_update⦈⦈⦈"
have "tee_memories (TEE_state s) = tee_memories (TEE_state (fst (subtractMgrInsRef s tid)))"
proof-
{
have a1: "(fst (subtractMgrInsRef s tid))
= s⦇TEE_state := (TEE_state s)⦇ta_mgr := (ta_mgr(TEE_state s))⦇mgr_ta_instances := ?mgrTaInsList_update⦈⦈⦈"
using subtractMgrInsRef_def
by (metis fst_conv)
then show ?thesis by auto
}
qed
} then show ?thesis by blast
qed
lemma tee_memories_removeAllSessIdInTaInsSessList: "∀s tid ses_id params_in params_out.
tee_memories (TEE_state s) = tee_memories (TEE_state (removeAllSessIdInTaInsSessList s tid ses_id params_in params_out))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?mgrTaInsCtxs = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?clientTaIns = "getTAInsCtx s tid"
let ?taSessList = "cur_ta_session_list ?clientTaIns"
let ?list_remove_sesId = "removeAll ses_id ?taSessList"
let ?taIns_update = "?clientTaIns⦇cur_ta_session_list := ?list_remove_sesId⦈"
let ?ta_index = "(SOME x. tid = cur_ta_thread_id (?mgrTaInsCtxs!x))"
let ?mgrTaInsList_update = "list_update ?mgrTaInsCtxs ?ta_index ?taIns_update"
let ?s_ret = "s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈"
have "tee_memories (TEE_state s) = tee_memories (TEE_state (removeAllSessIdInTaInsSessList s tid ses_id params_in params_out))"
proof-
{
have a1: "tee_memories (TEE_state s) = tee_memories (TEE_state (removeAllSessIdInTaInsSessList s tid ses_id params_in params_out))"
using removeAllSessIdInTaInsSessList_def
by (metis a111)
then show ?thesis by auto
}
qed
} then show ?thesis by blast
qed
lemma tee_memories_removeTaInsInMgrInsList: "∀s tid.
tee_memories (TEE_state s) = tee_memories (TEE_state (fst (removeTaInsInMgrInsList s tid)))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?isTaTidInList = "isTidInTaInsList ?mgrTaInsList tid"
let ?mgrTaInsList_removeAllTaInns = "removeAllTaInsInMgrInsList tid ?mgrTaInsList"
let ?s_ret = "s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_removeAllTaInns⦈⦈⦈"
have "tee_memories (TEE_state s) = tee_memories (TEE_state (fst (removeTaInsInMgrInsList s tid)))"
proof(cases "?isTaTidInList = False")
case True
have a1: "?isTaTidInList = False"
by (simp add: True)
then show ?thesis
proof-
{
have b1: "fst (removeTaInsInMgrInsList s tid) = s"
using removeTaInsInMgrInsList_def a1
by simp
then show ?thesis
by simp
}
qed
next
case False
have a2: "?isTaTidInList = True"
using False by auto
then show ?thesis
proof-
{
have c1: "fst (removeTaInsInMgrInsList s tid)
= s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_removeAllTaInns⦈⦈⦈"
using removeTaInsInMgrInsList_def a2
by simp
then show ?thesis by auto
}
qed
qed
} then show ?thesis by blast
qed
lemma tee_memories_addCloseSessionEvent: "∀sc s params_in params_out.
tee_memories (TEE_state s) = tee_memories (TEE_state (addCloseSessionEvent sc s params_in params_out sess))"
proof-
{
show ?thesis
proof(induction sess)
case Nil
then show ?case
by simp
next
case (Cons sesId sesIdLeft)
have "∀sc s params_in params_out.
tee_memories (TEE_state s) = tee_memories (TEE_state (addCloseSessionEvent sc s params_in params_out sesIdLeft))"
using Cons by auto
{
fix sc::"Sys_Config"
fix s::"State"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?s_closeCurTaInsSessList = "addCloseSessionEvent sc s params_in params_out (sesId#sesIdLeft)"
have a10: "?s_closeCurTaInsSessList =
(let
clientTa = ⦇login = KERN_IDENTITY, id = Some 1⦈;
nextFuncStepParam = ⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈;
s1 = s⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEE_CS2)#(exec_prime s)⦈
in
addCloseSessionEvent sc s1 params_in params_out sesIdLeft)"
by simp
have a11: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s_closeCurTaInsSessList)"
proof-
{
let ?clientTa = "⦇login = KERN_IDENTITY, id = Some 1⦈"
let ?nextFuncStepParam = "⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some ?clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈"
let ?s1 = "s⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEE_CS2)#(exec_prime s)⦈"
have b1: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s1)"
by simp
have b2: "tee_memories (TEE_state ?s_closeCurTaInsSessList) = tee_memories (TEE_state (addCloseSessionEvent sc ?s1 params_in params_out sesIdLeft))"
by simp
then show ?thesis using a10 Cons b1 b2
proof -
show ?thesis
using Cons.IH b1 b2 by presburger
qed
}
qed
}
then show ?case
by simp
qed
}
qed
lemma tee_memories_addCloseSessionEvent2: "∀sc s params_in params_out.
tee_memories (TEE_state s) = tee_memories (TEE_state (addCloseSessionEvent2 sc s params_in params_out sess))"
proof-
{
show ?thesis
proof(induction sess)
case Nil
then show ?case
by simp
next
case (Cons sesId sesIdLeft)
have "∀sc s params_in params_out.
tee_memories (TEE_state s) = tee_memories (TEE_state (addCloseSessionEvent2 sc s params_in params_out sesIdLeft))"
using Cons by auto
{
fix sc::"Sys_Config"
fix s::"State"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?s_closeCurTaInsSessList = "addCloseSessionEvent2 sc s params_in params_out (sesId#sesIdLeft)"
have a10: "?s_closeCurTaInsSessList =
(let
clientTa = ⦇login = KERN_IDENTITY, id = Some 1⦈;
nextFuncStepParam = ⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈;
s1 = s⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEEC_CS2)#(exec_prime s)⦈
in
addCloseSessionEvent2 sc s1 params_in params_out sesIdLeft)"
by simp
have a11: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s_closeCurTaInsSessList)"
proof-
{
let ?clientTa = "⦇login = KERN_IDENTITY, id = Some 1⦈"
let ?nextFuncStepParam = "⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some ?clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈"
let ?s1 = "s⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEEC_CS2)#(exec_prime s)⦈"
have b1: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s1)"
by simp
have b2: "tee_memories (TEE_state ?s_closeCurTaInsSessList) = tee_memories (TEE_state (addCloseSessionEvent2 sc ?s1 params_in params_out sesIdLeft))"
by simp
then show ?thesis using a10 Cons b1 b2
proof -
show ?thesis
using Cons.IH b1 b2 by presburger
qed
}
qed
}
then show ?case
by simp
qed
}
qed
lemma tee_memories_deleteTaStateByThreadId: "∀s tarTid.
tee_memories (TEE_state s) = tee_memories (TEE_state (deleteTaStateByThreadId s tarTid))"
proof-
{
fix s::"State"
fix tarTid::"THREAD_ID_TYPE"
let ?taState = "TAs_state s"
let ?taState_update = "?taState(tarTid := None)"
let ?s1 = "s⦇TAs_state := ?taState_update⦈"
have a1: "tee_memories (TEE_state (deleteTaStateByThreadId s tarTid))
= tee_memories (TEE_state (s⦇TAs_state := ?taState_update⦈))"
by (simp add: deleteTaStateByThreadId_def)
have a2: "tee_memories (TEE_state s)
= tee_memories (TEE_state (s⦇TAs_state := ?taState_update⦈))"
by simp
have a3: "tee_memories (TEE_state s) = tee_memories (TEE_state (deleteTaStateByThreadId s tarTid))"
by (metis a1 a2)
} then show ?thesis by blast
qed
lemma ree_total_size_deleteTaStateByThreadId: "∀s tarTid.
ree_total_size(REE_state s) = ree_total_size(REE_state (deleteTaStateByThreadId s tarTid))"
proof-
{
fix s::"State"
fix tarTid::"THREAD_ID_TYPE"
let ?taState = "TAs_state s"
let ?taState_update = "?taState(tarTid := None)"
let ?s1 = "s⦇TAs_state := ?taState_update⦈"
have a1: "ree_total_size(REE_state (deleteTaStateByThreadId s tarTid))
= ree_total_size(REE_state (s⦇TAs_state := ?taState_update⦈))"
by (simp add: deleteTaStateByThreadId_def)
have a2: "ree_total_size(REE_state s)
= ree_total_size(REE_state (s⦇TAs_state := ?taState_update⦈))"
by simp
have a3: "ree_total_size(REE_state s) = ree_total_size(REE_state (deleteTaStateByThreadId s tarTid))"
by (metis a1 a2)
} then show ?thesis by blast
qed
lemma isSessIdInTaStateSessList_ses_id: "∀ s ses_id t ses_id_t servTid servTid_t.
ses_id = ses_id_t ∧ servTid = servTid_t ∧ (TAs_state s) = (TAs_state t)
⟶ isSessIdInTaStateSessList s ses_id servTid = isSessIdInTaStateSessList s ses_id_t servTid_t"
proof-
{
fix s::"State"
fix t::"State"
fix ses_id::"SESSION_ID_TYPE option"
fix ses_id_t::"SESSION_ID_TYPE option"
fix servTid::"THREAD_ID_TYPE option"
fix servTid_t::"THREAD_ID_TYPE option"
let ?taState_s = "(TAs_state s) (the servTid)"
let ?taState_t = "(TAs_state s) (the servTid_t)"
let ?taSesListInTaState_s = "(TA_sessions (the ?taState_s))"
let ?taSesListInTaState_t = "(TA_sessions (the ?taState_t))"
let ?isSesIdInTaStateSesList_s = "isSesIdinSesIdList ?taSesListInTaState_s (the ses_id)"
let ?isSesIdInTaStateSesList_t = "isSesIdinSesIdList ?taSesListInTaState_t (the ses_id_t)"
assume a1: "ses_id = ses_id_t"
assume a2: "servTid = servTid_t"
assume a3: "(TAs_state s) = (TAs_state t)"
have b1: "?isSesIdInTaStateSesList_s = ?isSesIdInTaStateSesList_t"
by (simp add: a1 a2)
} then show ?thesis by auto
qed
lemma ree_total_size_addCloseSessionEvent2: "∀sc s params_in params_out.
ree_total_size(REE_state s) = ree_total_size(REE_state (addCloseSessionEvent2 sc s params_in params_out sess))"
proof-
{
show ?thesis
proof(induction sess)
case Nil
then show ?case
by simp
next
case (Cons sesId sesIdLeft)
have "∀sc s params_in params_out.
ree_total_size(REE_state s) = ree_total_size(REE_state (addCloseSessionEvent2 sc s params_in params_out sesIdLeft))"
using Cons by auto
{
fix sc::"Sys_Config"
fix s::"State"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?s_closeCurTaInsSessList = "addCloseSessionEvent2 sc s params_in params_out (sesId#sesIdLeft)"
have a10: "?s_closeCurTaInsSessList =
(let
clientTa = ⦇login = KERN_IDENTITY, id = Some 1⦈;
nextFuncStepParam = ⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈;
s1 = s⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEEC_CS2)#(exec_prime s)⦈
in
addCloseSessionEvent2 sc s1 params_in params_out sesIdLeft)"
by simp
have a11: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s_closeCurTaInsSessList)"
proof-
{
let ?clientTa = "⦇login = KERN_IDENTITY, id = Some 1⦈"
let ?nextFuncStepParam = "⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some ?clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈"
let ?s1 = "s⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEEC_CS2)#(exec_prime s)⦈"
have b1: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s1)"
by simp
have b2: "ree_total_size(REE_state ?s_closeCurTaInsSessList) = ree_total_size(REE_state (addCloseSessionEvent2 sc ?s1 params_in params_out sesIdLeft))"
by simp
then show ?thesis using a10 Cons b1 b2
proof -
show ?thesis
using Cons.IH b1 b2 by presburger
qed
}
qed
}
then show ?case
by simp
qed
}
qed
lemma ree_total_size_addCloseSessionEvent: "∀sc s params_in params_out.
ree_total_size(REE_state s) = ree_total_size(REE_state (addCloseSessionEvent sc s params_in params_out sess))"
proof-
{
show ?thesis
proof(induction sess)
case Nil
then show ?case
by simp
next
case (Cons sesId sesIdLeft)
have "∀sc s params_in params_out.
ree_total_size(REE_state s) = ree_total_size(REE_state (addCloseSessionEvent sc s params_in params_out sesIdLeft))"
using Cons by auto
{
fix sc::"Sys_Config"
fix s::"State"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?s_closeCurTaInsSessList = "addCloseSessionEvent sc s params_in params_out (sesId#sesIdLeft)"
have a10: "?s_closeCurTaInsSessList =
(let
clientTa = ⦇login = KERN_IDENTITY, id = Some 1⦈;
nextFuncStepParam = ⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈;
s1 = s⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEE_CS2)#(exec_prime s)⦈
in
addCloseSessionEvent sc s1 params_in params_out sesIdLeft)"
by simp
have a11: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s_closeCurTaInsSessList)"
proof-
{
let ?clientTa = "⦇login = KERN_IDENTITY, id = Some 1⦈"
let ?nextFuncStepParam = "⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some ?clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈"
let ?s1 = "s⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEE_CS2)#(exec_prime s)⦈"
have b1: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s1)"
by simp
have b2: "ree_total_size(REE_state ?s_closeCurTaInsSessList) = ree_total_size(REE_state (addCloseSessionEvent sc ?s1 params_in params_out sesIdLeft))"
by simp
then show ?thesis using a10 Cons b1 b2
proof -
show ?thesis
using Cons.IH b1 b2 by presburger
qed
}
qed
}
then show ?case
by simp
qed
}
qed
lemma driver_mem_addCloseSessionEvent: "∀sc s params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (addCloseSessionEvent sc s params_in params_out sess))"
proof-
{
show ?thesis
proof(induction sess)
case Nil
then show ?case
by simp
next
case (Cons sesId sesIdLeft)
have "∀sc s params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (addCloseSessionEvent sc s params_in params_out sesIdLeft))"
using Cons by auto
{
fix sc::"Sys_Config"
fix s::"State"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?s_closeCurTaInsSessList = "addCloseSessionEvent sc s params_in params_out (sesId#sesIdLeft)"
have a10: "?s_closeCurTaInsSessList =
(let
clientTa = ⦇login = KERN_IDENTITY, id = Some 1⦈;
nextFuncStepParam = ⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈;
s1 = s⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEE_CS2)#(exec_prime s)⦈
in
addCloseSessionEvent sc s1 params_in params_out sesIdLeft)"
by simp
have a11: "driver_mem(REE_state s) = driver_mem(REE_state ?s_closeCurTaInsSessList)"
proof-
{
let ?clientTa = "⦇login = KERN_IDENTITY, id = Some 1⦈"
let ?nextFuncStepParam = "⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some ?clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈"
let ?s1 = "s⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEE_CS2)#(exec_prime s)⦈"
have b1: "driver_mem(REE_state s) = driver_mem(REE_state ?s1)"
by simp
have b2: "driver_mem(REE_state ?s_closeCurTaInsSessList) = driver_mem(REE_state (addCloseSessionEvent sc ?s1 params_in params_out sesIdLeft))"
by simp
then show ?thesis using a10 Cons b1 b2
proof -
show ?thesis
using Cons.IH b1 b2 by presburger
qed
}
qed
}
then show ?case
by simp
qed
}
qed
lemma driver_mem_addCloseSessionEvent2: "∀sc s params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (addCloseSessionEvent2 sc s params_in params_out sess))"
proof-
{
show ?thesis
proof(induction sess)
case Nil
then show ?case
by simp
next
case (Cons sesId sesIdLeft)
have "∀sc s params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (addCloseSessionEvent2 sc s params_in params_out sesIdLeft))"
using Cons by auto
{
fix sc::"Sys_Config"
fix s::"State"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?s_closeCurTaInsSessList = "addCloseSessionEvent2 sc s params_in params_out (sesId#sesIdLeft)"
have a10: "?s_closeCurTaInsSessList =
(let
clientTa = ⦇login = KERN_IDENTITY, id = Some 1⦈;
nextFuncStepParam = ⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈;
s1 = s⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEEC_CS2)#(exec_prime s)⦈
in
addCloseSessionEvent2 sc s1 params_in params_out sesIdLeft)"
by simp
have a11: "driver_mem(REE_state s) = driver_mem(REE_state ?s_closeCurTaInsSessList)"
proof-
{
let ?clientTa = "⦇login = KERN_IDENTITY, id = Some 1⦈"
let ?nextFuncStepParam = "⦇param1 = Some sesId, param2 = None, param3 = None, param4 = Some ?clientTa,
param5 = None, param6 = None, param7 = Some params_in, param8 = Some params_out, param9 = None,
param10 = None, param11 = None, param12=None, param13=None⦈"
let ?s1 = "s⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEEC_CS2)#(exec_prime s)⦈"
have b1: "driver_mem(REE_state s) = driver_mem(REE_state ?s1)"
by simp
have b2: "driver_mem(REE_state ?s_closeCurTaInsSessList) = driver_mem(REE_state (addCloseSessionEvent2 sc ?s1 params_in params_out sesIdLeft))"
by simp
then show ?thesis using a10 Cons b1 b2
proof -
show ?thesis
using Cons.IH b1 b2 by presburger
qed
}
qed
}
then show ?case
by simp
qed
}
qed
lemma driver_mem_deleteTaStateByThreadId: "∀s tarTid.
driver_mem(REE_state s) = driver_mem(REE_state (deleteTaStateByThreadId s tarTid))"
proof-
{
fix s::"State"
fix tarTid::"THREAD_ID_TYPE"
let ?taState = "TAs_state s"
let ?taState_update = "?taState(tarTid := None)"
let ?s1 = "s⦇TAs_state := ?taState_update⦈"
have a1: "driver_mem(REE_state (deleteTaStateByThreadId s tarTid))
= driver_mem(REE_state (s⦇TAs_state := ?taState_update⦈))"
by (simp add: deleteTaStateByThreadId_def)
have a2: "driver_mem(REE_state s)
= driver_mem(REE_state (s⦇TAs_state := ?taState_update⦈))"
by simp
have a3: "driver_mem(REE_state s) = driver_mem(REE_state (deleteTaStateByThreadId s tarTid))"
by (metis a1 a2)
} then show ?thesis by blast
qed
lemma r111:"ree_total_size(REE_state s) = ree_total_size(REE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr:=(x::TEE_TA_MANAGER)⦈⦈))" by simp
lemma ree_total_size_removeAllSessIdInTaInsSessList: "∀s tid ses_id params_in params_out.
ree_total_size(REE_state s) = ree_total_size(REE_state (removeAllSessIdInTaInsSessList s tid ses_id params_in params_out))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?mgrTaInsCtxs = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?clientTaIns = "getTAInsCtx s tid"
let ?taSessList = "cur_ta_session_list ?clientTaIns"
let ?list_remove_sesId = "removeAll ses_id ?taSessList"
let ?taIns_update = "?clientTaIns⦇cur_ta_session_list := ?list_remove_sesId⦈"
let ?ta_index = "(SOME x. tid = cur_ta_thread_id (?mgrTaInsCtxs!x))"
let ?mgrTaInsList_update = "list_update ?mgrTaInsCtxs ?ta_index ?taIns_update"
let ?s_ret = "s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈"
have "ree_total_size(REE_state s) = ree_total_size(REE_state (removeAllSessIdInTaInsSessList s tid ses_id params_in params_out))"
proof-
{
have a1: "ree_total_size(REE_state s) = ree_total_size(REE_state (removeAllSessIdInTaInsSessList s tid ses_id params_in params_out))"
using removeAllSessIdInTaInsSessList_def
by (metis r111)
then show ?thesis by auto
}
qed
} then show ?thesis by blast
qed
lemma driver_mem_REE_state_mgr:"driver_mem(REE_state s) = driver_mem(REE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr:=(x::TEE_TA_MANAGER)⦈⦈))" by simp
lemma driver_mem_removeAllSessIdInTaInsSessList: "∀s tid ses_id params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (removeAllSessIdInTaInsSessList s tid ses_id params_in params_out))"
proof-
{
fix s::"State"
fix tid::"THREAD_ID_TYPE"
fix ses_id::"SESSION_ID_TYPE"
fix params_in::"PARAMS_TYPE"
fix params_out::"PARAMS_TYPE"
let ?mgrTaInsCtxs = "mgr_ta_instances (ta_mgr (TEE_state s))"
let ?clientTaIns = "getTAInsCtx s tid"
let ?taSessList = "cur_ta_session_list ?clientTaIns"
let ?list_remove_sesId = "removeAll ses_id ?taSessList"
let ?taIns_update = "?clientTaIns⦇cur_ta_session_list := ?list_remove_sesId⦈"
let ?ta_index = "(SOME x. tid = cur_ta_thread_id (?mgrTaInsCtxs!x))"
let ?mgrTaInsList_update = "list_update ?mgrTaInsCtxs ?ta_index ?taIns_update"
let ?s_ret = "s⦇TEE_state:=(TEE_state s)⦇ta_mgr := (ta_mgr (TEE_state s))⦇mgr_ta_instances:= ?mgrTaInsList_update⦈⦈⦈"
have "driver_mem(REE_state s) = driver_mem(REE_state (removeAllSessIdInTaInsSessList s tid ses_id params_in params_out))"
proof-
{
have a1: "driver_mem(REE_state s) = driver_mem(REE_state (removeAllSessIdInTaInsSessList s tid ses_id params_in params_out))"
using removeAllSessIdInTaInsSessList_def
by (metis driver_mem_REE_state_mgr)
then show ?thesis by auto
}
qed
} then show ?thesis by blast
qed
lemma tee_memories_tee_ta_close_session_teeDomain2 : "∀sc s tar_ses_id clientType params_in params_outs.
tee_memories (TEE_state s) = tee_memories (TEE_state (fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix tar_ses_id::"SESSION_ID_TYPE option"
fix open_sessions::"TA_MGR_SESSION_TYPE list"
fix clientType::"CLIENT_TYPE option"
fix params_in::"PARAMS_TYPE option"
fix params_out::"PARAMS_TYPE option"
let ?isSesIdinMgrSesIdList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the tar_ses_id)"
let ?client_type = "the clientType"
let ?params_in = "the params_in"
let ?params_out = "the params_out"
let ?ses_id = "the tar_ses_id"
let ?loginType = "login ?client_type"
let ?clnt_id_input = "id ?client_type"
let ?clientTid = "the(findSesCliTid s ?ses_id)"
let ?servTid = "the(findSesServTid s ?ses_id)"
let ?taMgrSes = "the(findMgrSessionFromList s ?ses_id)"
let ?taId_csess = "id(client_id ?taMgrSes)"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?s_close_session_teeDomain = "close_session_teeDomain2 sc ?s_setTaInsBusyByThreadId ?ses_id ?params_in ?params_out"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?nextFuncStepParam = "⦇param1 = tar_ses_id, param2 = Some ?servTid, param3 = None, param4 = clientType,
param5 = None, param6 =None, param7 = params_in, param8 = params_out, param9 = None, param10=None, param11=None,param12=None,param13=None⦈"
let ?s_callTa = "?s_setTaInsBusyByThreadId⦇current := ?servTid, exec_prime := (?nextFuncStepParam, TEEC_CS3)#(exec_prime ?s_setTaInsBusyByThreadId)⦈"
have "tee_memories (TEE_state s) =
tee_memories (TEE_state (fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)))"
proof(cases "tar_ses_id = None")
case True
have a1: "tar_ses_id = None"
using True by auto
then show ?thesis
proof-
{
have b1: "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = s"
using a1 tee_ta_close_session_teeDomain2_pre_def by simp
have b2: "tee_memories (TEE_state s) = tee_memories (TEE_state (fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)))"
by (simp add: b1)
then show ?thesis by simp
}
qed
next
case False
have a2: "tar_ses_id ≠ None"
using False by auto
then show ?thesis
proof(cases "?isSesIdinMgrSesIdList = False")
case True
then have "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = s"
using tee_ta_close_session_teeDomain2_pre_def
by simp
then show ?thesis
by simp
next
case False
then have a3: "¬(?isSesIdinMgrSesIdList = False)"
by simp
then show ?thesis
proof (cases "(?loginType = REE_PUBLIC ∧ ?clnt_id_input = None)
| ((?loginType = KERN_IDENTITY | ?loginType = DTC_IDENTITY))
| ((?loginType = TRUSTED_APP) ∧ ?clnt_id_input = ?taId_csess)")
case True
have a4: "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = ?s_callTa"
using tee_ta_close_session_teeDomain2_pre_def a3 a2 True
by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD)
have a5: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s_callTa)"
using a4
using setCurDomainAndEvent_def tee_memories_setTaInsBusy_setCurDomainAndEvent by fastforce
then show ?thesis using a4
by simp
next
case False
then have "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = s"
using tee_ta_close_session_teeDomain2_pre_def a3
by (smt (verit) eq_fst_iff)
then show ?thesis
by simp
qed
qed
qed
} then show ?thesis by auto
qed
lemma ree_total_size_tee_ta_close_session_teeDomain2 : "∀sc s ses_id client_type in_params out_params.
ree_total_size(REE_state s) = ree_total_size(REE_state (fst (tee_ta_close_session_teeDomain2_pre sc s ses_id client_type in_params out_params)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix tar_ses_id::"SESSION_ID_TYPE option"
fix open_sessions::"TA_MGR_SESSION_TYPE list"
fix clientType::"CLIENT_TYPE option"
fix params_in::"PARAMS_TYPE option"
fix params_out::"PARAMS_TYPE option"
let ?isSesIdinMgrSesIdList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the tar_ses_id)"
let ?client_type = "the clientType"
let ?params_in = "the params_in"
let ?params_out = "the params_out"
let ?ses_id = "the tar_ses_id"
let ?loginType = "login ?client_type"
let ?clnt_id_input = "id ?client_type"
let ?clientTid = "the(findSesCliTid s ?ses_id)"
let ?servTid = "the(findSesServTid s ?ses_id)"
let ?taMgrSes = "the(findMgrSessionFromList s ?ses_id)"
let ?taId_csess = "id(client_id ?taMgrSes)"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?s_close_session_teeDomain = "close_session_teeDomain2 sc ?s_setTaInsBusyByThreadId ?ses_id ?params_in ?params_out"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?nextFuncStepParam = "⦇param1 = tar_ses_id, param2 = Some ?servTid, param3 = None, param4 = clientType,
param5 = None, param6 =None, param7 = params_in, param8 = params_out, param9 = None, param10=None, param11=None,param12=None,param13=None⦈"
let ?s_callTa = "?s_setTaInsBusyByThreadId⦇current := ?servTid, exec_prime := (?nextFuncStepParam, TEEC_CS3)#(exec_prime ?s_setTaInsBusyByThreadId)⦈"
have "ree_total_size(REE_state s) =
ree_total_size(REE_state (fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)))"
proof(cases "tar_ses_id = None")
case True
have a1: "tar_ses_id = None"
using True by auto
then show ?thesis
proof-
{
have b1: "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = s"
using a1 tee_ta_close_session_teeDomain2_pre_def by simp
have b2: "ree_total_size(REE_state s) = ree_total_size(REE_state (fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)))"
by (simp add: b1)
then show ?thesis by simp
}
qed
next
case False
have a2: "tar_ses_id ≠ None"
using False by auto
then show ?thesis
proof(cases "?isSesIdinMgrSesIdList = False")
case True
then have "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = s"
using tee_ta_close_session_teeDomain2_pre_def
by simp
then show ?thesis
by simp
next
case False
then have a3: "¬(?isSesIdinMgrSesIdList = False)"
by simp
then show ?thesis
proof (cases "(?loginType = REE_PUBLIC ∧ ?clnt_id_input = None)
| ((?loginType = KERN_IDENTITY | ?loginType = DTC_IDENTITY))
| ((?loginType = TRUSTED_APP) ∧ ?clnt_id_input = ?taId_csess)")
case True
have a4: "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = ?s_callTa"
using tee_ta_close_session_teeDomain2_pre_def a3 a2 True
by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD)
have a5: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s_callTa)"
using a4
by (simp add: ree_total_size_setTaInsBusy)
then show ?thesis using a4
by simp
next
case False
then have "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = s"
using tee_ta_close_session_teeDomain2_pre_def a3
by (smt (verit) eq_fst_iff)
then show ?thesis
by simp
qed
qed
qed
} then show ?thesis by auto
qed
lemma driver_mem_tee_ta_close_session_teeDomain2 : "∀sc s tar_ses_id clientType params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix tar_ses_id::"SESSION_ID_TYPE option"
fix open_sessions::"TA_MGR_SESSION_TYPE list"
fix clientType::"CLIENT_TYPE option"
fix params_in::"PARAMS_TYPE option"
fix params_out::"PARAMS_TYPE option"
let ?isSesIdinMgrSesIdList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the tar_ses_id)"
let ?client_type = "the clientType"
let ?params_in = "the params_in"
let ?params_out = "the params_out"
let ?ses_id = "the tar_ses_id"
let ?loginType = "login ?client_type"
let ?clnt_id_input = "id ?client_type"
let ?clientTid = "the(findSesCliTid s ?ses_id)"
let ?servTid = "the(findSesServTid s ?ses_id)"
let ?taMgrSes = "the(findMgrSessionFromList s ?ses_id)"
let ?taId_csess = "id(client_id ?taMgrSes)"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?s_close_session_teeDomain = "close_session_teeDomain2 sc ?s_setTaInsBusyByThreadId ?ses_id ?params_in ?params_out"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?nextFuncStepParam = "⦇param1 = tar_ses_id, param2 = Some ?servTid, param3 = None, param4 = clientType,
param5 = None, param6 =None, param7 = params_in, param8 = params_out, param9 = None, param10=None, param11=None,param12=None,param13=None⦈"
let ?s_callTa = "?s_setTaInsBusyByThreadId⦇current := ?servTid, exec_prime := (?nextFuncStepParam, TEEC_CS3)#(exec_prime ?s_setTaInsBusyByThreadId)⦈"
have "driver_mem(REE_state s) =
driver_mem(REE_state (fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)))"
proof(cases "tar_ses_id = None")
case True
have a1: "tar_ses_id = None"
using True by auto
then show ?thesis
proof-
{
have b1: "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = s"
using a1 tee_ta_close_session_teeDomain2_pre_def
by simp
have b2: "driver_mem(REE_state s) = driver_mem(REE_state (fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)))"
by (simp add: b1)
then show ?thesis
by simp
}
qed
next
case False
have a2: "tar_ses_id ≠ None"
using False by auto
then show ?thesis
proof (cases "?isSesIdinMgrSesIdList = False")
case True
then show ?thesis using tee_ta_close_session_teeDomain2_pre_def
by simp
next
case False
have a3: "¬(?isSesIdinMgrSesIdList = False)" using False
by simp
then show ?thesis
proof (cases "(?loginType = REE_PUBLIC ∧ ?clnt_id_input = None)
| ((?loginType = KERN_IDENTITY | ?loginType = DTC_IDENTITY))
| ((?loginType = TRUSTED_APP) ∧ ?clnt_id_input = ?taId_csess)")
case True
have a4: "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = ?s_callTa"
using a2 a3 True tee_ta_close_session_teeDomain2_pre_def
by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD)
have a5: "driver_mem(REE_state s) = driver_mem(REE_state ?s_callTa)"
using a4
by (simp add: driver_mem_tee_setTaInsBusy)
then show ?thesis using a4
by simp
next
case False
have "(fst (tee_ta_close_session_teeDomain2_pre sc s tar_ses_id clientType params_in params_out)) = s"
using a2 a3 False tee_ta_close_session_teeDomain2_pre_def
by auto
then show ?thesis
by simp
qed
qed
qed
} then show ?thesis by auto
qed
subsubsection "TEE_CloseTASession2_new"
lemma tee_memories_tee_ta_close_session_teeDomain : "∀sc s tar_ses_id clientType params_in params_outs.
tee_memories (TEE_state s) = tee_memories (TEE_state (fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix tar_ses_id::"SESSION_ID_TYPE option"
fix open_sessions::"TA_MGR_SESSION_TYPE list"
fix clientType::"CLIENT_TYPE option"
fix params_in::"PARAMS_TYPE option"
fix params_out::"PARAMS_TYPE option"
let ?isSesIdinMgrSesIdList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the tar_ses_id)"
let ?client_type = "the clientType"
let ?params_in = "the params_in"
let ?params_out = "the params_out"
let ?ses_id = "the tar_ses_id"
let ?loginType = "login ?client_type"
let ?clnt_id_input = "id ?client_type"
let ?clientTid = "the(findSesCliTid s ?ses_id)"
let ?servTid = "the(findSesServTid s ?ses_id)"
let ?taMgrSes = "the(findMgrSessionFromList s ?ses_id)"
let ?taId_csess = "id(client_id ?taMgrSes)"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?s_close_session_teeDomain = "close_session_teeDomain2 sc ?s_setTaInsBusyByThreadId ?ses_id ?params_in ?params_out"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?nextFuncStepParam = "⦇param1 = tar_ses_id, param2 = Some ?servTid, param3 = None, param4 = clientType,
param5 = None, param6 =None, param7 = params_in, param8 = params_out, param9 = None, param10=None, param11=None,param12=None,param13=None⦈"
let ?s_callTa = "?s_setTaInsBusyByThreadId⦇current := ?servTid, exec_prime := (?nextFuncStepParam, TEE_CS3)#(exec_prime ?s_setTaInsBusyByThreadId)⦈"
have "tee_memories (TEE_state s) =
tee_memories (TEE_state (fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)))"
proof(cases "tar_ses_id = None")
case True
have a1: "tar_ses_id = None"
using True by auto
then show ?thesis
proof-
{
have b1: "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = s"
using a1 tee_ta_close_session_teeDomain_pre_def by simp
have b2: "tee_memories (TEE_state s) = tee_memories (TEE_state (fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)))"
by (simp add: b1)
then show ?thesis by simp
}
qed
next
case False
have a2: "tar_ses_id ≠ None"
using False by auto
then show ?thesis
proof(cases "?isSesIdinMgrSesIdList = False")
case True
then have "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = s"
using tee_ta_close_session_teeDomain_pre_def
by simp
then show ?thesis
by simp
next
case False
then have a3: "¬(?isSesIdinMgrSesIdList = False)"
by simp
then show ?thesis
proof (cases "(?loginType = REE_PUBLIC ∧ ?clnt_id_input = None)
| ((?loginType = KERN_IDENTITY | ?loginType = DTC_IDENTITY))
| ((?loginType = TRUSTED_APP) ∧ ?clnt_id_input = ?taId_csess)")
case True
have a4: "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = ?s_callTa"
using tee_ta_close_session_teeDomain_pre_def a3 a2 True
by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD)
have a5: "tee_memories (TEE_state s) = tee_memories (TEE_state ?s_callTa)"
using a4
using setCurDomainAndEvent_def tee_memories_setTaInsBusy_setCurDomainAndEvent by fastforce
then show ?thesis using a4
by simp
next
case False
then have "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = s"
using tee_ta_close_session_teeDomain_pre_def a3
by (smt (verit) eq_fst_iff)
then show ?thesis
by simp
qed
qed
qed
} then show ?thesis by auto
qed
lemma ree_total_size_tee_ta_close_session_teeDomain : "∀sc s ses_id client_type in_params out_params.
ree_total_size(REE_state s) = ree_total_size(REE_state (fst (tee_ta_close_session_teeDomain_pre sc s ses_id client_type in_params out_params)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix tar_ses_id::"SESSION_ID_TYPE option"
fix open_sessions::"TA_MGR_SESSION_TYPE list"
fix clientType::"CLIENT_TYPE option"
fix params_in::"PARAMS_TYPE option"
fix params_out::"PARAMS_TYPE option"
let ?isSesIdinMgrSesIdList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the tar_ses_id)"
let ?client_type = "the clientType"
let ?params_in = "the params_in"
let ?params_out = "the params_out"
let ?ses_id = "the tar_ses_id"
let ?loginType = "login ?client_type"
let ?clnt_id_input = "id ?client_type"
let ?clientTid = "the(findSesCliTid s ?ses_id)"
let ?servTid = "the(findSesServTid s ?ses_id)"
let ?taMgrSes = "the(findMgrSessionFromList s ?ses_id)"
let ?taId_csess = "id(client_id ?taMgrSes)"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?s_close_session_teeDomain = "close_session_teeDomain2 sc ?s_setTaInsBusyByThreadId ?ses_id ?params_in ?params_out"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?nextFuncStepParam = "⦇param1 = tar_ses_id, param2 = Some ?servTid, param3 = None, param4 = clientType,
param5 = None, param6 =None, param7 = params_in, param8 = params_out, param9 = None, param10=None, param11=None,param12=None,param13=None⦈"
let ?s_callTa = "?s_setTaInsBusyByThreadId⦇current := ?servTid, exec_prime := (?nextFuncStepParam, TEE_CS3)#(exec_prime ?s_setTaInsBusyByThreadId)⦈"
have "ree_total_size(REE_state s) =
ree_total_size(REE_state (fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)))"
proof(cases "tar_ses_id = None")
case True
have a1: "tar_ses_id = None"
using True by auto
then show ?thesis
proof-
{
have b1: "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = s"
using a1 tee_ta_close_session_teeDomain_pre_def by simp
have b2: "ree_total_size(REE_state s) = ree_total_size(REE_state (fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)))"
by (simp add: b1)
then show ?thesis by simp
}
qed
next
case False
have a2: "tar_ses_id ≠ None"
using False by auto
then show ?thesis
proof(cases "?isSesIdinMgrSesIdList = False")
case True
then have "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = s"
using tee_ta_close_session_teeDomain_pre_def
by simp
then show ?thesis
by simp
next
case False
then have a3: "¬(?isSesIdinMgrSesIdList = False)"
by simp
then show ?thesis
proof (cases "(?loginType = REE_PUBLIC ∧ ?clnt_id_input = None)
| ((?loginType = KERN_IDENTITY | ?loginType = DTC_IDENTITY))
| ((?loginType = TRUSTED_APP) ∧ ?clnt_id_input = ?taId_csess)")
case True
have a4: "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = ?s_callTa"
using tee_ta_close_session_teeDomain_pre_def a3 a2 True
by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD)
have a5: "ree_total_size(REE_state s) = ree_total_size(REE_state ?s_callTa)"
using a4
by (simp add: ree_total_size_setTaInsBusy)
then show ?thesis using a4
by simp
next
case False
then have "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = s"
using tee_ta_close_session_teeDomain_pre_def a3
by (smt (verit) eq_fst_iff)
then show ?thesis
by simp
qed
qed
qed
} then show ?thesis by auto
qed
lemma driver_mem_tee_ta_close_session_teeDomain : "∀sc s tar_ses_id clientType params_in params_out.
driver_mem(REE_state s) = driver_mem(REE_state (fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)))"
proof-
{
fix sc::"Sys_Config"
fix s::"State"
fix tar_ses_id::"SESSION_ID_TYPE option"
fix open_sessions::"TA_MGR_SESSION_TYPE list"
fix clientType::"CLIENT_TYPE option"
fix params_in::"PARAMS_TYPE option"
fix params_out::"PARAMS_TYPE option"
let ?isSesIdinMgrSesIdList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the tar_ses_id)"
let ?client_type = "the clientType"
let ?params_in = "the params_in"
let ?params_out = "the params_out"
let ?ses_id = "the tar_ses_id"
let ?loginType = "login ?client_type"
let ?clnt_id_input = "id ?client_type"
let ?clientTid = "the(findSesCliTid s ?ses_id)"
let ?servTid = "the(findSesServTid s ?ses_id)"
let ?taMgrSes = "the(findMgrSessionFromList s ?ses_id)"
let ?taId_csess = "id(client_id ?taMgrSes)"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?s_close_session_teeDomain = "close_session_teeDomain2 sc ?s_setTaInsBusyByThreadId ?ses_id ?params_in ?params_out"
let ?s_setTaInsBusyByThreadId = "setTaInsBusyByThreadId s ?servTid True"
let ?nextFuncStepParam = "⦇param1 = tar_ses_id, param2 = Some ?servTid, param3 = None, param4 = clientType,
param5 = None, param6 =None, param7 = params_in, param8 = params_out, param9 = None, param10=None, param11=None,param12=None,param13=None⦈"
let ?s_callTa = "?s_setTaInsBusyByThreadId⦇current := ?servTid, exec_prime := (?nextFuncStepParam, TEE_CS3)#(exec_prime ?s_setTaInsBusyByThreadId)⦈"
have "driver_mem(REE_state s) =
driver_mem(REE_state (fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)))"
proof(cases "tar_ses_id = None")
case True
have a1: "tar_ses_id = None"
using True by auto
then show ?thesis
proof-
{
have b1: "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = s"
using a1 tee_ta_close_session_teeDomain_pre_def
by simp
have b2: "driver_mem(REE_state s) = driver_mem(REE_state (fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)))"
by (simp add: b1)
then show ?thesis
by simp
}
qed
next
case False
have a2: "tar_ses_id ≠ None"
using False by auto
then show ?thesis
proof (cases "?isSesIdinMgrSesIdList = False")
case True
then show ?thesis using tee_ta_close_session_teeDomain_pre_def
by simp
next
case False
have a3: "¬(?isSesIdinMgrSesIdList = False)" using False
by simp
then show ?thesis
proof (cases "(?loginType = REE_PUBLIC ∧ ?clnt_id_input = None)
| ((?loginType = KERN_IDENTITY | ?loginType = DTC_IDENTITY))
| ((?loginType = TRUSTED_APP) ∧ ?clnt_id_input = ?taId_csess)")
case True
have a4: "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = ?s_callTa"
using a2 a3 True tee_ta_close_session_teeDomain_pre_def
by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD)
have a5: "driver_mem(REE_state s) = driver_mem(REE_state ?s_callTa)"
using a4
by (simp add: driver_mem_tee_setTaInsBusy)
then show ?thesis using a4
by simp
next
case False
have "(fst (tee_ta_close_session_teeDomain_pre sc s tar_ses_id clientType params_in params_out)) = s"
using a2 a3 False tee_ta_close_session_teeDomain_pre_def
by auto
then show ?thesis
by simp
qed
qed
qed
} then show ?thesis by auto
qed
end